defpred S1[ 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 S1[x,y,z] ) from 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
thus NonTerminals G c= [:1,5:] :: according to XBOOLE_0:def 10 :: thesis:
proof
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 ;
hence x in [:1,5:] by A2, A5, A7; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:1,5:] or x in NonTerminals G )
assume A8: x in [:1,5:] ; :: thesis:
then reconsider t = x as Symbol of G by ;
t ==> <*t,t*> by A2, A8;
hence x in NonTerminals G by A3; :: thesis: verum
end;
then A9: G is with_nonterminals by DTCONSTR:def 4;
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:
proof
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:
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 ;
then t ==> <*t,t*> by A2;
hence contradiction by A13; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Data-Loc or x in Terminals G )
assume A14: x in SCM-Data-Loc ; :: thesis:
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 ;
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 ;
then x in [:1,5:] by ;
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 ;
hence contradiction by A15, XTUPLE_0:1; :: thesis: verum
end;
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
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 ;
A21: root-tree d1 in TS G by ;
root-tree d0 in TS G by ;
then reconsider p = <*(),()*> as FinSequence of TS G by ;
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 = <*(() . {}),(() . {})*> by DTCONSTR:6
.= <*(() . {}),d1*> by TREES_4:3
.= <*d0,d1*> by TREES_4:3 ;
hence nt ==> roots p by A2, A4, A22; :: thesis: verum
end;
then A23: G is with_useful_nonterminals by DTCONSTR:def 5;
G is with_terminals by ;
hence ex b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st
( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) ) by A2, A11, A4, A9, A23; :: thesis: verum