let G be non empty with_terminals with_nonterminals DTConstrStr ; :: thesis: for tsg being Element of TS G
for nt being NonTerminal of G st tsg . {} = nt holds
ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
defpred S2[ DecoratedTree of the carrier of G] means for nt being NonTerminal of G st $1 . {} = nt holds
ex ts being FinSequence of TS G st
( $1 = nt -tree ts & nt ==> roots ts );
A1: now :: thesis: for s being Symbol of G st s in Terminals G holds
S2[ root-tree s]
let s be Symbol of G; :: thesis: ( s in Terminals G implies S2[ root-tree s] )
assume A2: s in Terminals G ; :: thesis: S2[ root-tree s]
thus S2[ root-tree s] :: thesis: verum
proof
let nt be NonTerminal of G; :: thesis: ( (root-tree s) . {} = nt implies ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts ) )
assume (root-tree s) . {} = nt ; :: thesis: ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts )
then A3: s = nt by TREES_4:3;
Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
then A4: ex t being Symbol of G st
( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A2;
A5: nt in NonTerminals G ;
NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
then ex t being Symbol of G st
( nt = t & ex tnt being FinSequence st t ==> tnt ) by A5;
hence ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts ) by A3, A4; :: thesis: verum
end;
end;
A6: now :: thesis: for nnt being Symbol of G
for tts being FinSequence of TS G st nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ) holds
S2[nnt -tree tts]
let nnt be Symbol of G; :: thesis: for tts being FinSequence of TS G st nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ) holds
S2[nnt -tree tts]
let tts be FinSequence of TS G; :: thesis: ( nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ) implies S2[nnt -tree tts] )
assume that
A7: nnt ==> roots tts and
for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ; :: thesis: S2[nnt -tree tts]
thus S2[nnt -tree tts] :: thesis: verum
proof
let nt be NonTerminal of G; :: thesis: ( (nnt -tree tts) . {} = nt implies ex ts being FinSequence of TS G st
( nnt -tree tts = nt -tree ts & nt ==> roots ts ) )
assume A8: (nnt -tree tts) . {} = nt ; :: thesis: ex ts being FinSequence of TS G st
( nnt -tree tts = nt -tree ts & nt ==> roots ts )
take ts = tts; :: thesis: ( nnt -tree tts = nt -tree ts & nt ==> roots ts )
thus ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) by A7, A8, TREES_4:def 4; :: thesis: verum
end;
end;
A9: for t being DecoratedTree of the carrier of G st t in TS G holds
S2[t] from DTCONSTR:sch 7(A1, A6);
 let tsg be Element of TS G; :: thesis: for nt being NonTerminal of G st tsg . {} = nt holds
ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
let nt be NonTerminal of G; :: thesis: ( tsg . {} = nt implies ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts ) )
assume tsg . {} = nt ; :: thesis: ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
hence ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts ) by A9; :: thesis: verum