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 ] 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
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;
( 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 ) ;
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;
A5: now
let nnt be Symbol of G; :: thesis: for tts being FinSequence of TS G st nnt ==> roots tts & ( for t being DecoratedTree of 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 st t in rng tts holds
S2[t] ) implies S2[nnt -tree tts] )
assume A6: ( nnt ==> roots tts & ( for t being DecoratedTree of 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 A7: (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 A6, A7, TREES_4:def 4; :: thesis: verum
end;
end;
A8: for t being DecoratedTree of st t in TS G holds
S2[t] from DTCONSTR:sch 7(A1, A5);
 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 A8; :: thesis: verum