reconsider 01 = {0,1} as non empty set ;

reconsider a90 = 0 , a91 = 1 as Element of 01 by TARSKI:def 2;

reconsider a9119 = <*a91*> ^ <*a91*> as Element of 01 * ;

reconsider P = {[a90,a9119]} as Relation of 01,(01 *) ;

take cherry = DTConstrStr(# 01,P #); :: thesis: ( cherry is binary & cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

reconsider a90 = a90, a91 = a91 as Symbol of cherry ;

then A3: a91 in Terminals cherry by LANG1:def 2;

thus Terminals cherry <> {} by A2, LANG1:def 2; :: according to DTCONSTR:def 3 :: thesis: ( cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

[a90,a9119] in P by TARSKI:def 1;

then a90 ==> a9119 by LANG1:def 1;

then a90 in { t where t is Symbol of cherry : ex s being FinSequence st t ==> s } ;

hence NonTerminals cherry <> {} by LANG1:def 3; :: according to DTCONSTR:def 4 :: thesis: ( cherry is with_useful_nonterminals & cherry is strict )

A4: { s where s is Symbol of cherry : ex p being FinSequence st s ==> p } = NonTerminals cherry by LANG1:def 3;

reconsider a90 = 0 , a91 = 1 as Element of 01 by TARSKI:def 2;

reconsider a9119 = <*a91*> ^ <*a91*> as Element of 01 * ;

reconsider P = {[a90,a9119]} as Relation of 01,(01 *) ;

take cherry = DTConstrStr(# 01,P #); :: thesis: ( cherry is binary & cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

reconsider a90 = a90, a91 = a91 as Symbol of cherry ;

hereby :: according to BINTREE1:def 4 :: thesis: ( cherry is with_terminals & cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

let s be Symbol of cherry; :: thesis: for p being FinSequence st s ==> p holds

ex x1, x2 being Symbol of cherry st p = <*x1,x2*>

let p be FinSequence; :: thesis: ( s ==> p implies ex x1, x2 being Symbol of cherry st p = <*x1,x2*> )

assume A1: s ==> p ; :: thesis: ex x1, x2 being Symbol of cherry st p = <*x1,x2*>

take x1 = a91; :: thesis: ex x2 being Symbol of cherry st p = <*x1,x2*>

take x2 = a91; :: thesis: p = <*x1,x2*>

[s,p] in P by A1, LANG1:def 1;

then [s,p] = [0,a9119] by TARSKI:def 1;

then p = a9119 by XTUPLE_0:1

.= <*1,1*> by FINSEQ_1:def 9 ;

hence p = <*x1,x2*> ; :: thesis: verum

end;ex x1, x2 being Symbol of cherry st p = <*x1,x2*>

let p be FinSequence; :: thesis: ( s ==> p implies ex x1, x2 being Symbol of cherry st p = <*x1,x2*> )

assume A1: s ==> p ; :: thesis: ex x1, x2 being Symbol of cherry st p = <*x1,x2*>

take x1 = a91; :: thesis: ex x2 being Symbol of cherry st p = <*x1,x2*>

take x2 = a91; :: thesis: p = <*x1,x2*>

[s,p] in P by A1, LANG1:def 1;

then [s,p] = [0,a9119] by TARSKI:def 1;

then p = a9119 by XTUPLE_0:1

.= <*1,1*> by FINSEQ_1:def 9 ;

hence p = <*x1,x2*> ; :: thesis: verum

now :: thesis: for s being FinSequence holds not a91 ==> s

then A2:
a91 in { t where t is Symbol of cherry : for s being FinSequence holds not t ==> s }
;let s be FinSequence; :: thesis: not a91 ==> s

assume a91 ==> s ; :: thesis: contradiction

then [1,s] in P by LANG1:def 1;

then [1,s] = [0,a9119] by TARSKI:def 1;

hence contradiction by XTUPLE_0:1; :: thesis: verum

end;assume a91 ==> s ; :: thesis: contradiction

then [1,s] in P by LANG1:def 1;

then [1,s] = [0,a9119] by TARSKI:def 1;

hence contradiction by XTUPLE_0:1; :: thesis: verum

then A3: a91 in Terminals cherry by LANG1:def 2;

thus Terminals cherry <> {} by A2, LANG1:def 2; :: according to DTCONSTR:def 3 :: thesis: ( cherry is with_nonterminals & cherry is with_useful_nonterminals & cherry is strict )

[a90,a9119] in P by TARSKI:def 1;

then a90 ==> a9119 by LANG1:def 1;

then a90 in { t where t is Symbol of cherry : ex s being FinSequence st t ==> s } ;

hence NonTerminals cherry <> {} by LANG1:def 3; :: according to DTCONSTR:def 4 :: thesis: ( cherry is with_useful_nonterminals & cherry is strict )

A4: { s where s is Symbol of cherry : ex p being FinSequence st s ==> p } = NonTerminals cherry by LANG1:def 3;

hereby :: according to DTCONSTR:def 5 :: thesis: cherry is strict

thus
cherry is strict
; :: thesis: verumreconsider X = TS cherry as non empty set by A3, DTCONSTR:def 1;

let nt be Symbol of cherry; :: thesis: ( nt in NonTerminals cherry implies ex q9 being FinSequence of TS cherry st nt ==> roots q9 )

reconsider rt1 = root-tree a91 as Element of X by A3, DTCONSTR:def 1;

reconsider q = <*rt1*> ^ <*rt1*> as FinSequence of TS cherry ;

q = <*(root-tree 1),(root-tree 1)*> by FINSEQ_1:def 9;

then A5: roots q = <*((root-tree a91) . {}),((root-tree a91) . {})*> by DTCONSTR:6;

assume nt in NonTerminals cherry ; :: thesis: ex q9 being FinSequence of TS cherry st nt ==> roots q9

then ex s being Symbol of cherry st

( nt = s & ex p being FinSequence st s ==> p ) by A4;

then consider p being FinSequence such that

A6: nt ==> p ;

take q9 = q; :: thesis: nt ==> roots q9

[nt,p] in P by A6, LANG1:def 1;

then A7: [nt,p] = [0,a9119] by TARSKI:def 1;

( a9119 = <*1,1*> & (root-tree 1) . {} = 1 ) by FINSEQ_1:def 9, TREES_4:3;

hence nt ==> roots q9 by A6, A7, A5, XTUPLE_0:1; :: thesis: verum

end;let nt be Symbol of cherry; :: thesis: ( nt in NonTerminals cherry implies ex q9 being FinSequence of TS cherry st nt ==> roots q9 )

reconsider rt1 = root-tree a91 as Element of X by A3, DTCONSTR:def 1;

reconsider q = <*rt1*> ^ <*rt1*> as FinSequence of TS cherry ;

q = <*(root-tree 1),(root-tree 1)*> by FINSEQ_1:def 9;

then A5: roots q = <*((root-tree a91) . {}),((root-tree a91) . {})*> by DTCONSTR:6;

assume nt in NonTerminals cherry ; :: thesis: ex q9 being FinSequence of TS cherry st nt ==> roots q9

then ex s being Symbol of cherry st

( nt = s & ex p being FinSequence st s ==> p ) by A4;

then consider p being FinSequence such that

A6: nt ==> p ;

take q9 = q; :: thesis: nt ==> roots q9

[nt,p] in P by A6, LANG1:def 1;

then A7: [nt,p] = [0,a9119] by TARSKI:def 1;

( a9119 = <*1,1*> & (root-tree 1) . {} = 1 ) by FINSEQ_1:def 9, TREES_4:3;

hence nt ==> roots q9 by A6, A7, A5, XTUPLE_0:1; :: thesis: verum