consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that
A1: PreTraversal (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) = <*nt*> ^ (FlattenSeq x) by Def12;
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 & PreTraversal t = ((height (dom t)) |-> 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 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 & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> )
thus root-tree s = t by A5, Lm10, TARSKI:def 1; :: thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
thus PreTraversal t = <*O*> by A1, A2
.= {} ^ <*O*> by FINSEQ_1:34
.= (0 |-> 1) ^ <*0*>
.= ((height (dom t)) |-> 1) ^ <*0*> 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 & PreTraversal t9 = ((height (dom t9)) |-> 1) ^ <*0*> ) by A8;
f . x9 is Element of the carrier of PeanoNat * ;
then A13: f . x9 = ((height (dom x9)) |-> 1) ^ <*0*> by A2, A3, A12, Def12;
f * ts = <*(f . x)*> by A10, FINSEQ_2:35;
then A14: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq <*(f . x9)*>) by A3, A7
.= <*nt*> ^ (((height (dom x9)) |-> 1) ^ <*0*>) by A13, PRE_POLY:1
.= (<*nt*> ^ ((height (dom x9)) |-> 1)) ^ <*0*> by FINSEQ_1:32
.= ((1 |-> 1) ^ ((height (dom x9)) |-> 1)) ^ <*0*> by A9, FINSEQ_2:59
.= (((height (dom x9)) + 1) |-> 1) ^ <*0*> by FINSEQ_2:123
.= ((height (^ (dom x9))) |-> 1) ^ <*0*> 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 PreTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def12;
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: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
S2[t] by A17;
hence PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> ; :: thesis: verum