defpred S2[ DecoratedTree of the carrier of PeanoNat] means $1 = NAT-to-PN . (PN-to-NAT . $1);
A3:
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 A4:
nt ==> roots ts
and A5:
for
t being
DecoratedTree of the
carrier of
PeanoNat st
t in rng ts holds
S2[
t]
;
S2[nt -tree ts]A6:
nt <> O
by A4, Lm8;
(
roots ts = <*O*> or
roots ts = <*S*> )
by A4, Def2;
then
len (roots ts) = 1
by FINSEQ_1:40;
then consider dt being
Element of
FinTrees the
carrier of
PeanoNat such that A7:
ts = <*dt*>
and A8:
dt in TS PeanoNat
by Th5;
reconsider dt =
dt as
Element of
TS PeanoNat by A8;
rng ts = {dt}
by A7, FINSEQ_1:38;
then
dt in rng ts
by TARSKI:def 1;
then A9:
dt = NAT-to-PN . (PN-to-NAT . dt)
by A5;
A10:
PN-to-NAT * ts = <*(PN-to-NAT . dt)*>
by A7, FINSEQ_2:35;
set N =
PN-to-NAT . dt;
A11:
plus-one <*(PN-to-NAT . dt)*> = (PN-to-NAT . dt) + 1
by FINSEQ_1:40;
NAT-to-PN . ((PN-to-NAT . dt) + 1) =
PNsucc dt
by A9, Def10
.=
nt -tree ts
by A6, A7, Lm2, TARSKI:def 2
;
hence
S2[
nt -tree ts]
by A4, A10, A11, Def8;
verum end;
for t being DecoratedTree of the carrier of PeanoNat 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)
; verum