consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that
A1: PostTraversal (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
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> by Def13;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means ex t being Element of TS PeanoNat st
( $1 = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) );
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 A5: s in Terminals PeanoNat ; :: thesis: S2[ root-tree s]
thus S2[ root-tree s] :: thesis: verum
proof
take t = rtO; :: thesis: ( root-tree s = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) )
thus root-tree s = t by A5, Lm10, TARSKI:def 1; :: thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
thus PostTraversal t = <*O*> by A1, A2
.= <*O*> ^ {} by FINSEQ_1:34
.= <*0*> ^ (0 |-> 1)
.= <*0*> ^ ((height (dom t)) |-> 1) by TREES_1:42, TREES_4:3 ; :: thesis: verum
end;
end;
A6: 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
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; :: thesis: S2[nt -tree ts]
reconsider t9 = nt -tree ts as Element of TS PeanoNat by A7, Def1;
A9: nt = S by A7, Def2;
( roots ts = <*O*> or roots ts = <*1*> ) by A7, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A10: ts = <*x*> and
A11: x in TS PeanoNat by Th5;
reconsider x9 = x as Element of TS PeanoNat by A11;
rng ts = {x} by A10, FINSEQ_1:39;
then x in rng ts by TARSKI:def 1;
then A12: ex t9 being Element of TS PeanoNat st
( x = t9 & PostTraversal t9 = <*O*> ^ ((height (dom t9)) |-> 1) ) by A8;
f . x9 is Element of the carrier of PeanoNat * ;
then A13: f . x9 = <*O*> ^ ((height (dom x9)) |-> 1) by A2, A3, A12, Def13;
f * ts = <*(f . x)*> by A10, FINSEQ_2:35;
then A14: f . (nt -tree ts) = (FlattenSeq <*(f . x9)*>) ^ <*nt*> by A3, A7
.= (<*O*> ^ ((height (dom x9)) |-> 1)) ^ <*nt*> by A13, PRE_POLY:1
.= <*O*> ^ (((height (dom x9)) |-> 1) ^ <*nt*>) by FINSEQ_1:32
.= <*O*> ^ (((height (dom x9)) |-> 1) ^ (1 |-> 1)) by A9, FINSEQ_2:59
.= <*O*> ^ (((height (dom x9)) + 1) |-> 1) by FINSEQ_2:123
.= <*O*> ^ ((height (^ (dom x9))) |-> 1) by TREES_3:80 ;
A15: dom (nt -tree x9) = ^ (dom x9) by TREES_4:13;
A16: t9 = nt -tree x9 by A10, TREES_4:def 5;
f . t9 is Element of the carrier of PeanoNat * ;
then PostTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def13;
hence S2[nt -tree ts] by A14, A15, A16; :: thesis: verum
end;
A17: for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch 7(A4, A6);
 let t be Element of TS PeanoNat; :: thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
S2[t] by A17;
hence PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) ; :: thesis: verum