scheme :: BINTREE1:sch 2
BinDTConstrInd{ F1() -> non empty with_terminals with_nonterminals binary DTConstrStr , P1[ set ] } :
for t being Element of TS F1() holds P1[t]
provided
A1: for s being Terminal of F1() holds P1[ root-tree s] and
A2: for nt being NonTerminal of F1()
for tl, tr being Element of TS F1() st nt ==> <*(root-label tl),(root-label tr)*> & P1[tl] & P1[tr] holds
P1[nt -tree (tl,tr)]