scheme :: DTCONSTR:sch 8
DTConstrIndDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2() } :
ex f being Function of (TS F1()),F2() st
( ( for t being Symbol of F1() st t in Terminals F1() holds
f . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
f . (nt -tree ts) = F4(nt,(roots ts),(f * ts)) ) )