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) );
A6:
now 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;
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;
( 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]
;
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;
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; PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
S2[t]
by A17;
hence
PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
; verum