scheme :: BINTREE1:sch 3
BinDTConstrIndDef{ F₁() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F₂() -> non empty set , F₃( set ) -> Element of F₂(), F₄( set , set , set , set , set ) -> Element of F₂() } :

ex f being Function of (TS F₁()),F₂() st
( ( for t being Terminal of F₁() holds f . (root-tree t) = F₃(t) ) & ( for nt being NonTerminal of F₁()
for tl, tr being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F₄(nt,rtl,rtr,xl,xr) ) )