scheme :: MSAFREE1:sch 1
DTConstrUniq{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of (TS F1()),F2(), F6() -> Function of (TS F1()),F2() } :
F5() = F6()
provided
A1: for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) and
A2: for nt being Symbol of F1()
for ts being Element of (TS F1()) * st nt ==> roots ts holds
for x being Element of F2() * st x = F5() * ts holds
F5() . (nt -tree ts) = F4(nt,ts,x) and
A3: for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) and
A4: for nt being Symbol of F1()
for ts being Element of (TS F1()) * st nt ==> roots ts holds
for x being Element of F2() * st x = F6() * ts holds
F6() . (nt -tree ts) = F4(nt,ts,x)