scheme :: BINTREE1:sch 4
BinDTConstrUniqDef{ F₁() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F₂() -> non empty set , F₃() -> Function of (TS F₁()),F₂(), F₄() -> Function of (TS F₁()),F₂(), F₅( set ) -> Element of F₂(), F₆( set , set , set , set , set ) -> Element of F₂() } :

F₃() = F₄()

provided

A1: ( ( 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) ) ) and
A2: ( ( 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) ) )