consider f being Function of (TS PeanoNat),((Terminals PeanoNat) *) such that
A1:
TerminalString (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 st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts)
by Def11;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means TerminalString $1 = <*0*>;
A5:
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 A6:
nt ==> roots ts
and A7:
for
t being
DecoratedTree of the
carrier of
PeanoNat st
t in rng ts holds
S2[
t]
;
S2[nt -tree ts]A8:
nt -tree ts in TS PeanoNat
by A6, Def1;
(
roots ts = <*O*> or
roots ts = <*1*> )
by A6, Def2;
then
len (roots ts) = 1
by FINSEQ_1:40;
then consider x being
Element of
FinTrees the
carrier of
PeanoNat such that A9:
ts = <*x*>
and A10:
x in TS PeanoNat
by Th5;
reconsider x9 =
x as
Element of
TS PeanoNat by A10;
rng ts = {x}
by A9, FINSEQ_1:39;
then A11:
x in rng ts
by TARSKI:def 1;
f . x9 is
Element of
(Terminals PeanoNat) *
;
then A12:
f . x9 =
TerminalString x
by A2, A3, Def11
.=
<*O*>
by A7, A11
;
f * ts = <*(f . x)*>
by A9, FINSEQ_2:35;
then f . (nt -tree ts) =
FlattenSeq <*(f . x9)*>
by A3, A6
.=
<*O*>
by A12, PRE_POLY:1
;
hence
S2[
nt -tree ts]
by A2, A3, A8, Def11;
verum end;
thus
for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t]
from DTCONSTR:sch 7(A4, A5); verum