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

F₄() = F₅()

provided

A1: ( ( for t being Terminal of F₁() ex g being Function of F₂(),F₃() st
( g = F₄() . (root-tree t) & ( for a being Element of F₂() holds g . a = F₆(t,a) ) ) ) & ( for nt being NonTerminal of F₁()
for t1, t2 being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F₂(),F₃() st
( g = F₄() . (nt -tree (t1,t2)) & f1 = F₄() . t1 & f2 = F₄() . t2 & ( for a being Element of F₂() holds g . a = F₇(nt,f1,f2,a) ) ) ) ) and
A2: ( ( for t being Terminal of F₁() ex g being Function of F₂(),F₃() st
( g = F₅() . (root-tree t) & ( for a being Element of F₂() holds g . a = F₆(t,a) ) ) ) & ( for nt being NonTerminal of F₁()
for t1, t2 being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F₂(),F₃() st
( g = F₅() . (nt -tree (t1,t2)) & f1 = F₅() . t1 & f2 = F₅() . t2 & ( for a being Element of F₂() holds g . a = F₇(nt,f1,f2,a) ) ) ) )