scheme :: BINTREE1:sch 2
BinDTConstrInd{ F₁() -> non empty with_terminals with_nonterminals binary DTConstrStr , P₁[ set ] } :

for t being Element of TS F₁() holds P₁[t]

provided

A1: for s being Terminal of F₁() holds P₁[ root-tree s] and
A2: for nt being NonTerminal of F₁()
for tl, tr being Element of TS F₁() st nt ==> <*(root-label tl),(root-label tr)*> & P₁[tl] & P₁[tr] holds
P₁[nt -tree (tl,tr)]