defpred S2[ DecoratedTree of ] means $1 = NAT-to-PN . (PN-to-NAT . $1);
A3:
now let nt be
Symbol of
PeanoNat ;
:: thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of 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 st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )assume A4:
(
nt ==> roots ts & ( for
t being
DecoratedTree of st
t in rng ts holds
S2[
t] ) )
;
:: thesis: S2[nt -tree ts]then A5:
nt <> O
by Lm7;
(
roots ts = <*O*> or
roots ts = <*S*> )
by A4, Def5;
then
len (roots ts) = 1
by FINSEQ_1:57;
then consider dt being
Element of
FinTrees the
carrier of
PeanoNat such that A6:
(
ts = <*dt*> &
dt in TS PeanoNat )
by Th5;
reconsider dt =
dt as
Element of
TS PeanoNat by A6;
rng ts = {dt}
by A6, FINSEQ_1:55;
then
dt in rng ts
by TARSKI:def 1;
then A7:
dt = NAT-to-PN . (PN-to-NAT . dt)
by A4;
A8:
PN-to-NAT * ts = <*(PN-to-NAT . dt)*>
by A6, FINSEQ_2:39;
reconsider N =
PN-to-NAT . dt as
Element of
NAT ;
reconsider x =
<*N*> as
FinSequence of
NAT ;
consider n being
Element of
NAT such that A9:
(
plus-one x = n + 1 &
<*N*> . 1
= n )
by Def10;
N = n
by A9, FINSEQ_1:57;
then NAT-to-PN . (n + 1) =
PNsucc dt
by A7, Def13
.=
nt -tree ts
by A5, A6, Lm2, TARSKI:def 2
;
hence
S2[
nt -tree ts]
by A4, A8, A9, Def11;
:: thesis: verum end;
for t being DecoratedTree of st t in TS PeanoNat holds
S2[t]
from DTCONSTR:sch 7(A1, A3);
hence
for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)
; :: thesis: verum