begin
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( set , set , set ) -> Element of NAT = 0 ;
Lm1: dom (roots {}) =
dom {}
by TREES_3:def 18
.=
{}
;
begin
scheme
DTCMin{
F1()
-> Function,
F2()
-> non
empty DTConstrStr ,
F3()
-> non
empty set ,
F4(
set )
-> Element of
F3(),
F5(
set ,
set ,
set )
-> Element of
F3() } :
ex
X being
Subset of
(FinTrees [: the carrier of F2(),F3():]) st
(
X = Union F1() & ( for
d being
Symbol of
F2() st
d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for
o being
Symbol of
F2()
for
p being
FinSequence of
X st
o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for
F being
Subset of
(FinTrees [: the carrier of F2(),F3():]) st ( for
d being
Symbol of
F2() st
d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for
o being
Symbol of
F2()
for
p being
FinSequence of
F st
o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
provided
begin
defpred S1[ set , set ] means ( $1 = 1 & ( $2 = <*0*> or $2 = <*1*> ) );
set PN = PeanoNat ;
Lm2:
the carrier of PeanoNat = {0,1}
by Def2;
then reconsider O = 0 , S = 1 as Symbol of PeanoNat by TARSKI:def 2;
Lm3:
S ==> <*O*>
by Def2;
Lm4:
S ==> <*S*>
by Def2;
Lm5:
S ==> <*O*>
by Def2;
Lm6:
S ==> <*S*>
by Def2;
Lm7:
Terminals PeanoNat = { x where x is Symbol of PeanoNat : for tnt being FinSequence holds not x ==> tnt }
by LANG1:def 2;
then Lm9:
O in Terminals PeanoNat
by Lm7;
Lm10:
Terminals PeanoNat c= {O}
Lm11:
NonTerminals PeanoNat = { x where x is Symbol of PeanoNat : ex tnt being FinSequence st x ==> tnt }
by LANG1:def 3;
then Lm12:
S in NonTerminals PeanoNat
by Lm5;
then Lm13:
{S} c= NonTerminals PeanoNat
by ZFMISC_1:31;
Lm14:
NonTerminals PeanoNat c= {S}
then Lm15:
NonTerminals PeanoNat = {S}
by Lm13, XBOOLE_0:def 10;
reconsider TSPN = TS PeanoNat as non empty Subset of (FinTrees the carrier of PeanoNat) by Def1, Lm9;
begin
Lm16:
( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
begin
set PN = PeanoNat ;
reconsider O = O as Terminal of PeanoNat by Lm9;
reconsider S = S as NonTerminal of PeanoNat by Lm12;
deffunc H3( set , set , FinSequence of NAT ) -> Element of NAT = plus-one $3;
deffunc H4( set , Element of TS PeanoNat) -> Element of TS PeanoNat = PNsucc $2;
Lm17: 0 =
PN-to-NAT . (root-tree O)
by Def8
.=
PN-to-NAT . (NAT-to-PN . 0)
by Def10
;
begin
definition
let G be non
empty DTConstrStr ;
let tsg be
DecoratedTree of the
carrier of
G;
assume A1:
tsg in TS G
;
defpred S2[
set ]
means $1
in Terminals G;
deffunc H5(
set )
-> set =
<*$1*>;
deffunc H6(
set )
-> set =
{} ;
consider s2t being
Function of the
carrier of
G,
((Terminals G) *) such that A4:
for
s being
set st
s in the
carrier of
G holds
( (
S2[
s] implies
s2t . s = H5(
s) ) & ( not
S2[
s] implies
s2t . s = H6(
s) ) )
from FUNCT_2:sch 5(A2);
deffunc H7(
Symbol of
G)
-> Element of
(Terminals G) * =
s2t . $1;
deffunc H8(
set ,
set ,
FinSequence of
(Terminals G) * )
-> Element of
(Terminals G) * =
FlattenSeq $3;
deffunc H9(
set )
-> set =
<*$1*>;
existence
ex b1 being FinSequence of Terminals G ex f being Function of (TS G),((Terminals G) *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )
uniqueness
for b1, b2 being FinSequence of Terminals G st ex f being Function of (TS G),((Terminals G) *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) & ex f being Function of (TS G),((Terminals G) *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) holds
b1 = b2
consider s2s being
Function of the
carrier of
G,
( the carrier of G *) such that A18:
for
s being
set st
s in the
carrier of
G holds
s2s . s = H9(
s)
from FUNCT_2:sch 2(A17);
deffunc H10(
Symbol of
G)
-> Element of the
carrier of
G * =
s2s . $1;
deffunc H11(
Symbol of
G,
set ,
FinSequence of the
carrier of
G * )
-> Element of the
carrier of
G * =
(s2s . $1) ^ (FlattenSeq $3);
existence
ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) )
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) & ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) holds
b1 = b2
deffunc H12(
Symbol of
G)
-> Element of the
carrier of
G * =
s2s . $1;
deffunc H13(
Symbol of
G,
set ,
FinSequence of the
carrier of
G * )
-> Element of the
carrier of
G * =
(FlattenSeq $3) ^ (s2s . $1);
existence
ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) & ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) holds
b1 = b2
end;