let G, G9 be non empty DTConstrStr ; :: thesis: ( Terminals G c= Terminals G9 & the Rules of G c= the Rules of G9 implies TS G c= TS G9 )
assume that
A1: Terminals G c= Terminals G9 and
A2: the Rules of G c= the Rules of G9 ; :: thesis: TS G c= TS G9
A3: the carrier of G9 = (Terminals G9) \/ (NonTerminals G9) by LANG1:1;
A4: the carrier of G c= the carrier of G9 by A1, A2, Th115;
defpred S1[ set ] means $1 in TS G9;
A5: for s being Symbol of G st s in Terminals G holds
S1[ root-tree s]
proof
let s be Symbol of G; :: thesis: ( s in Terminals G implies S1[ root-tree s] )
assume A6: s in Terminals G ; :: thesis: S1[ root-tree s]
then reconsider s9 = s as Symbol of G9 by A1, A3, XBOOLE_0:def 3;
root-tree s = root-tree s9 ;
hence S1[ root-tree s] by A1, A6, DTCONSTR:def 1; :: thesis: verum
end;
A7: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let n be Symbol of G; :: thesis: for ts being FinSequence of TS G st n ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S1[t] ) holds
S1[n -tree ts]
let s be FinSequence of TS G; :: thesis: ( n ==> roots s & ( for t being DecoratedTree of the carrier of G st t in rng s holds
S1[t] ) implies S1[n -tree s] )
assume that
A8: [n,(roots s)] in the Rules of G and
A9: for t being DecoratedTree of the carrier of G st t in rng s holds
S1[t] ; :: according to LANG1:def 1 :: thesis: S1[n -tree s]
rng s c= TS G9 by A9;
then reconsider s9 = s as FinSequence of TS G9 by FINSEQ_1:def 4;
reconsider n9 = n as Symbol of G9 by A4;
n9 ==> roots s9 by A2, A8;
hence S1[n -tree s] by DTCONSTR:def 1; :: thesis: verum
end;
A10: for t being DecoratedTree of the carrier of G st t in TS G holds
S1[t] from DTCONSTR:sch 7(A5, A7);
 let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TS G or x in TS G9 )
assume A11: x in TS G ; :: thesis: x in TS G9
then reconsider t = x as Element of FinTrees the carrier of G ;
S1[t] by A10, A11;
hence x in TS G9 ; :: thesis: verum