defpred S_{1}[ set , set , set ] means $1 in [:1,5:];

consider G being non empty strict binary DTConstrStr such that

A1: the carrier of G = SCM-Data-Loc \/ [:1,5:] and

A2: for x, y, z being Symbol of G holds

( x ==> <*y,z*> iff S_{1}[x,y,z] )
from BINTREE1:sch 1();

A3: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;

A4: NonTerminals G = [:1,5:]

A10: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;

A11: Terminals G = SCM-Data-Loc

G is with_terminals by A11, DTCONSTR:def 3;

hence ex b_{1} being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st

( Terminals b_{1} = SCM-Data-Loc & NonTerminals b_{1} = [:1,5:] & ( for x, y, z being Symbol of b_{1} holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) ) by A2, A11, A4, A9, A23; :: thesis: verum

consider G being non empty strict binary DTConstrStr such that

A1: the carrier of G = SCM-Data-Loc \/ [:1,5:] and

A2: for x, y, z being Symbol of G holds

( x ==> <*y,z*> iff S

A3: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;

A4: NonTerminals G = [:1,5:]

proof

then A9:
G is with_nonterminals
by DTCONSTR:def 4;
thus
NonTerminals G c= [:1,5:]
:: according to XBOOLE_0:def 10 :: thesis: [:1,5:] c= NonTerminals G

assume A8: x in [:1,5:] ; :: thesis: x in NonTerminals G

then reconsider t = x as Symbol of G by A1, XBOOLE_0:def 3;

t ==> <*t,t*> by A2, A8;

hence x in NonTerminals G by A3; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:1,5:] or x in NonTerminals G )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals G or x in [:1,5:] )

assume x in NonTerminals G ; :: thesis: x in [:1,5:]

then consider t being Symbol of G such that

A5: x = t and

A6: ex tnt being FinSequence st t ==> tnt by A3;

consider tnt being FinSequence such that

A7: t ==> tnt by A6;

ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A7, BINTREE1:def 4;

hence x in [:1,5:] by A2, A5, A7; :: thesis: verum

end;assume x in NonTerminals G ; :: thesis: x in [:1,5:]

then consider t being Symbol of G such that

A5: x = t and

A6: ex tnt being FinSequence st t ==> tnt by A3;

consider tnt being FinSequence such that

A7: t ==> tnt by A6;

ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A7, BINTREE1:def 4;

hence x in [:1,5:] by A2, A5, A7; :: thesis: verum

assume A8: x in [:1,5:] ; :: thesis: x in NonTerminals G

then reconsider t = x as Symbol of G by A1, XBOOLE_0:def 3;

t ==> <*t,t*> by A2, A8;

hence x in NonTerminals G by A3; :: thesis: verum

A10: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;

A11: Terminals G = SCM-Data-Loc

proof

thus
Terminals G c= SCM-Data-Loc
:: according to XBOOLE_0:def 10 :: thesis: SCM-Data-Loc c= Terminals G

assume A14: x in SCM-Data-Loc ; :: thesis: x in Terminals G

then A15: ex y, z being object st

( y in {1} & z in NAT & x = [y,z] ) by ZFMISC_1:84;

reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def 3;

assume not x in Terminals G ; :: thesis: contradiction

then consider tnt being FinSequence such that

A16: t ==> tnt by A10;

ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A16, BINTREE1:def 4;

then x in [:1,5:] by A2, A16;

then consider x1, x2 being object such that

A17: x1 in 1 and

x2 in 5 and

A18: x = [x1,x2] by ZFMISC_1:84;

x = [0,x2] by A17, A18, CARD_1:49, TARSKI:def 1;

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

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Data-Loc or x in Terminals G )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals G or x in SCM-Data-Loc )

assume x in Terminals G ; :: thesis: x in SCM-Data-Loc

then consider t being Symbol of G such that

A12: x = t and

A13: for tnt being FinSequence holds not t ==> tnt by A10;

assume not x in SCM-Data-Loc ; :: thesis: contradiction

then t in [:1,5:] by A1, A12, XBOOLE_0:def 3;

then t ==> <*t,t*> by A2;

hence contradiction by A13; :: thesis: verum

end;assume x in Terminals G ; :: thesis: x in SCM-Data-Loc

then consider t being Symbol of G such that

A12: x = t and

A13: for tnt being FinSequence holds not t ==> tnt by A10;

assume not x in SCM-Data-Loc ; :: thesis: contradiction

then t in [:1,5:] by A1, A12, XBOOLE_0:def 3;

then t ==> <*t,t*> by A2;

hence contradiction by A13; :: thesis: verum

assume A14: x in SCM-Data-Loc ; :: thesis: x in Terminals G

then A15: ex y, z being object st

( y in {1} & z in NAT & x = [y,z] ) by ZFMISC_1:84;

reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def 3;

assume not x in Terminals G ; :: thesis: contradiction

then consider tnt being FinSequence such that

A16: t ==> tnt by A10;

ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A16, BINTREE1:def 4;

then x in [:1,5:] by A2, A16;

then consider x1, x2 being object such that

A17: x1 in 1 and

x2 in 5 and

A18: x = [x1,x2] by ZFMISC_1:84;

x = [0,x2] by A17, A18, CARD_1:49, TARSKI:def 1;

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

now :: thesis: for nt being Symbol of G st nt in NonTerminals G holds

ex p being FinSequence of TS G st nt ==> roots p

then A23:
G is with_useful_nonterminals
by DTCONSTR:def 5;ex p being FinSequence of TS G st nt ==> roots p

A19:
dl. 1 in SCM-Data-Loc
by AMI_2:def 16;

A20: dl. 0 in SCM-Data-Loc by AMI_2:def 16;

then reconsider d0 = dl. 0, d1 = dl. 1 as Symbol of G by A1, A19, XBOOLE_0:def 3;

A21: root-tree d1 in TS G by A11, A19, DTCONSTR:def 1;

root-tree d0 in TS G by A11, A20, DTCONSTR:def 1;

then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by A21, FINSEQ_2:13;

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

assume A22: nt in NonTerminals G ; :: thesis: ex p being FinSequence of TS G st nt ==> roots p

take p = p; :: thesis: nt ==> roots p

roots p = <*((root-tree d0) . {}),((root-tree d1) . {})*> by DTCONSTR:6

.= <*((root-tree d0) . {}),d1*> by TREES_4:3

.= <*d0,d1*> by TREES_4:3 ;

hence nt ==> roots p by A2, A4, A22; :: thesis: verum

end;A20: dl. 0 in SCM-Data-Loc by AMI_2:def 16;

then reconsider d0 = dl. 0, d1 = dl. 1 as Symbol of G by A1, A19, XBOOLE_0:def 3;

A21: root-tree d1 in TS G by A11, A19, DTCONSTR:def 1;

root-tree d0 in TS G by A11, A20, DTCONSTR:def 1;

then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by A21, FINSEQ_2:13;

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

assume A22: nt in NonTerminals G ; :: thesis: ex p being FinSequence of TS G st nt ==> roots p

take p = p; :: thesis: nt ==> roots p

roots p = <*((root-tree d0) . {}),((root-tree d1) . {})*> by DTCONSTR:6

.= <*((root-tree d0) . {}),d1*> by TREES_4:3

.= <*d0,d1*> by TREES_4:3 ;

hence nt ==> roots p by A2, A4, A22; :: thesis: verum

G is with_terminals by A11, DTCONSTR:def 3;

hence ex b

( Terminals b

( x ==> <*y,z*> iff x in [:1,5:] ) ) ) by A2, A11, A4, A9, A23; :: thesis: verum