consider f being Function of (TS PeanoNat),((Terminals PeanoNat) *) such that
A1: TerminalString (root-tree O) = f . (root-tree O) and
A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = <*t*> and
A3: for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) by Def11;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means TerminalString $1 = <*0*>;
A4: now :: thesis: for s being Symbol of PeanoNat st s in Terminals PeanoNat holds
S2[ root-tree s]
let s be Symbol of PeanoNat; :: thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] )
assume s in Terminals PeanoNat ; :: thesis: S2[ root-tree s]
then s = O by Lm10, TARSKI:def 1;
hence S2[ root-tree s] by A1, A2; :: thesis: verum
end;
A5: now :: thesis: for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let nt be Symbol of PeanoNat; :: thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS PeanoNat; :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; :: thesis: S2[nt -tree ts]
A8: nt -tree ts in TS PeanoNat by A6, Def1;
( roots ts = <*O*> or roots ts = <*1*> ) by A6, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A9: ts = <*x*> and
A10: x in TS PeanoNat by Th5;
reconsider x9 = x as Element of TS PeanoNat by A10;
rng ts = {x} by A9, FINSEQ_1:39;
then A11: x in rng ts by TARSKI:def 1;
f . x9 is Element of (Terminals PeanoNat) * ;
then A12: f . x9 = TerminalString x by A2, A3, Def11
.= <*O*> by A7, A11 ;
f * ts = <*(f . x)*> by A9, FINSEQ_2:35;
then f . (nt -tree ts) = FlattenSeq <*(f . x9)*> by A3, A6
.= <*O*> by A12, PRE_POLY:1 ;
hence S2[nt -tree ts] by A2, A3, A8, Def11; :: thesis: verum
end;
thus for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch 7(A4, A5); :: thesis: verum