:: On Defining Functions on Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 12, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

deffunc H1( set ) -> Element of NAT = 0 ;

deffunc H2( set , set , set ) -> Element of NAT = 0 ;

theorem Th1: :: DTCONSTR:1
for D being non empty set
for p being FinSequence of FinTrees D holds p is FinSequence of Trees D
proof end;

theorem Th2: :: DTCONSTR:2
for x, y being set
for p being FinSequence of x st y in dom p holds
p . y in x
proof end;

registration
let D be non empty set ;
let T be DTree-set of D;
cluster -> DTree-yielding for FinSequence of T;
coherence
for b1 being FinSequence of T holds b1 is DTree-yielding
;
end;

definition
let D be non empty set ;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
:: original: Element
redefine mode Element of Tset -> Element of F;
coherence
for b1 being Element of Tset holds b1 is Element of F
proof end;
end;

definition
let D be non empty set ;
let T be DTree-set of D;
let p be FinSequence of T;
:: original: roots
redefine func roots p -> FinSequence of D;
coherence
roots p is FinSequence of D
proof end;
end;

Lm1: dom (roots {}) = dom {} by TREES_3:def 18
.= {} ;

theorem Th3: :: DTCONSTR:3
roots {} = {} by Lm1;

theorem Th4: :: DTCONSTR:4
for T being DecoratedTree holds roots <*T*> = <*(T . {})*>
proof end;

theorem Th5: :: DTCONSTR:5
for D being non empty set
for F being Subset of (FinTrees D)
for p being FinSequence of F st len (roots p) = 1 holds
ex x being Element of FinTrees D st
( p = <*x*> & x in F )
proof end;

theorem :: DTCONSTR:6
for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>
proof end;

definition
let X, Y be set ;
let f be FinSequence of [:X,Y:];
:: original: pr1
redefine func pr1 f -> FinSequence of X;
coherence
pr1 f is FinSequence of X
proof end;
:: original: pr2
redefine func pr2 f -> FinSequence of Y;
coherence
pr2 f is FinSequence of Y
proof end;
end;

theorem Th7: :: DTCONSTR:7
( pr1 {} = {} & pr2 {} = {} )
proof end;

begin

registration
let A be non empty set ;
let R be Relation of A,(A *);
cluster DTConstrStr(# A,R #) -> non empty ;
coherence
not DTConstrStr(# A,R #) is empty
;
end;

scheme :: DTCONSTR:sch 1
DTConstrStrEx{ F1() -> non empty set , P1[ set , set ] } :
ex G being non empty strict DTConstrStr st
( the carrier of G = F1() & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P1[x,p] ) ) )
proof end;

scheme :: DTCONSTR:sch 2
DTConstrStrUniq{ F1() -> non empty set , P1[ set , set ] } :
for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = F1() & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] ) ) & the carrier of G2 = F1() & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P1[x,p] ) ) holds
G1 = G2
proof end;

theorem :: DTCONSTR:8
for G being non empty DTConstrStr holds Terminals G misses NonTerminals G
proof end;

scheme :: DTCONSTR:sch 3
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
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) )
}
proof end;

scheme :: DTCONSTR:sch 4
DTCSymbols{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex X1 being Subset of (FinTrees the carrier of F2()) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) & ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) )
}
proof end;

scheme :: DTCONSTR:sch 5
DTCHeight{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for n being Element of NAT
for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . n iff height (dom dt) <= n )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) )
}
proof end;

scheme :: DTCONSTR:sch 6
DTCUniq{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 holds
dt1 = dt2
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) )
}
proof end;

definition
let G be non empty DTConstrStr ;
func TS G -> Subset of (FinTrees the carrier of G) means :Def1: :: DTCONSTR:def 1
( ( for d being Symbol of G st d in Terminals G holds
root-tree d in it ) & ( for o being Symbol of G
for p being FinSequence of it st o ==> roots p holds
o -tree p in it ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
it c= F ) );
existence
ex b1 being Subset of (FinTrees the carrier of G) st
( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b1 ) & ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b1 c= F ) )
proof end;
uniqueness
for b1, b2 being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in b1 ) & ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines TS DTCONSTR:def 1 :
for G being non empty DTConstrStr
for b2 being Subset of (FinTrees the carrier of G) holds
( b2 = TS G iff ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) ) );

scheme :: DTCONSTR:sch 7
DTConstrInd{ F1() -> non empty DTConstrStr , P1[ set ] } :
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
P1[t]
provided
A1: for s being Symbol of F1() st s in Terminals F1() holds
P1[ root-tree s] and
A2: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof end;

scheme :: DTCONSTR:sch 8
DTConstrIndDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2() } :
ex f being Function of (TS F1()),F2() st
( ( for t being Symbol of F1() st t in Terminals F1() holds
f . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
f . (nt -tree ts) = F4(nt,(roots ts),(f * ts)) ) )
proof end;

scheme :: DTCONSTR:sch 9
DTConstrUniqDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of (TS F1()),F2(), F6() -> Function of (TS F1()),F2() } :
F5() = F6()
provided
A1: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F5() . (nt -tree ts) = F4(nt,(roots ts),(F5() * ts)) ) ) and
A2: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F6() . (nt -tree ts) = F4(nt,(roots ts),(F6() * ts)) ) )
proof end;

begin

defpred S1[ set , set ] means ( $1 = 1 & ( $2 = <*0*> or $2 = <*1*> ) );

definition
func PeanoNat -> non empty strict DTConstrStr means :Def2: :: DTCONSTR:def 2
( the carrier of it = {0,1} & ( for x being Symbol of it
for y being FinSequence of the carrier of it holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) );
existence
ex b1 being non empty strict DTConstrStr st
( the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict DTConstrStr st the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) & the carrier of b2 = {0,1} & ( for x being Symbol of b2
for y being FinSequence of the carrier of b2 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines PeanoNat DTCONSTR:def 2 :
for b1 being non empty strict DTConstrStr holds
( b1 = PeanoNat iff ( the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*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;

Lm8: now :: thesis: for x being FinSequence holds not O ==> x
given x being FinSequence such that A1: O ==> x ; :: thesis: contradiction
[O,x] in the Rules of PeanoNat by A1, LANG1:def 1;
then x in the carrier of PeanoNat * by ZFMISC_1:87;
then x is FinSequence of the carrier of PeanoNat by FINSEQ_2:def 3;
hence contradiction by A1, Def2; :: thesis: verum
end;

then Lm9: O in Terminals PeanoNat
by Lm7;

Lm10: Terminals PeanoNat c= {O}
proof end;

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}
proof end;

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

:: Some properties of decorated tree constructions
definition
let G be non empty DTConstrStr ;
attr G is with_terminals means :Def3: :: DTCONSTR:def 3
Terminals G <> {} ;
attr G is with_nonterminals means :Def4: :: DTCONSTR:def 4
NonTerminals G <> {} ;
attr G is with_useful_nonterminals means :Def5: :: DTCONSTR:def 5
for nt being Symbol of G st nt in NonTerminals G holds
ex p being FinSequence of TS G st nt ==> roots p;
end;

:: deftheorem Def3 defines with_terminals DTCONSTR:def 3 :
for G being non empty DTConstrStr holds
( G is with_terminals iff Terminals G <> {} );

:: deftheorem Def4 defines with_nonterminals DTCONSTR:def 4 :
for G being non empty DTConstrStr holds
( G is with_nonterminals iff NonTerminals G <> {} );

:: deftheorem Def5 defines with_useful_nonterminals DTCONSTR:def 5 :
for G being non empty DTConstrStr holds
( G is with_useful_nonterminals iff for nt being Symbol of G st nt in NonTerminals G holds
ex p being FinSequence of TS G st nt ==> roots p );

Lm16: ( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
proof end;

registration
cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals for DTConstrStr ;
existence
ex b1 being non empty DTConstrStr st
( b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict )
by Lm16;
end;

definition
let G be non empty with_terminals DTConstrStr ;
:: original: Terminals
redefine func Terminals G -> non empty Subset of G;
coherence
Terminals G is non empty Subset of G
proof end;
end;

registration
let G be non empty with_terminals DTConstrStr ;
cluster TS G -> non empty ;
coherence
not TS G is empty
proof end;
end;

registration
let G be non empty with_useful_nonterminals DTConstrStr ;
cluster TS G -> non empty ;
coherence
not TS G is empty
proof end;
end;

definition
let G be non empty with_nonterminals DTConstrStr ;
:: original: NonTerminals
redefine func NonTerminals G -> non empty Subset of G;
coherence
NonTerminals G is non empty Subset of G
proof end;
end;

definition
let G be non empty with_terminals DTConstrStr ;
mode Terminal of G is Element of Terminals G;
end;

definition
let G be non empty with_nonterminals DTConstrStr ;
mode NonTerminal of G is Element of NonTerminals G;
end;

definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
mode SubtreeSeq of nt -> FinSequence of TS G means :Def6: :: DTCONSTR:def 6
nt ==> roots it;
existence
ex b1 being FinSequence of TS G st nt ==> roots b1
by Def5;
end;

:: deftheorem Def6 defines SubtreeSeq DTCONSTR:def 6 :
for G being non empty with_nonterminals with_useful_nonterminals DTConstrStr
for nt being NonTerminal of G
for b3 being FinSequence of TS G holds
( b3 is SubtreeSeq of nt iff nt ==> roots b3 );

definition
let G be non empty with_terminals DTConstrStr ;
let t be Terminal of G;
:: original: root-tree
redefine func root-tree t -> Element of TS G;
coherence
root-tree t is Element of TS G
by Def1;
end;

definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
let p be SubtreeSeq of nt;
:: original: -tree
redefine func nt -tree p -> Element of TS G;
coherence
nt -tree p is Element of TS G
proof end;
end;

theorem Th9: :: DTCONSTR:9
for G being non empty with_terminals DTConstrStr
for tsg being Element of TS G
for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
proof end;

theorem Th10: :: DTCONSTR:10
for G being non empty with_terminals with_nonterminals DTConstrStr
for tsg being Element of TS G
for nt being NonTerminal of G st tsg . {} = nt holds
ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
proof end;

begin

:: Peano naturals continued
registration
cluster PeanoNat -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
by Lm16;
end;

set PN = PeanoNat ;

reconsider O = O as Terminal of PeanoNat by Lm9;

reconsider S = S as NonTerminal of PeanoNat by Lm12;

definition
let nt be NonTerminal of PeanoNat;
let t be Element of TS PeanoNat;
:: original: -tree
redefine func nt -tree t -> Element of TS PeanoNat;
coherence
nt -tree t is Element of TS PeanoNat
proof end;
end;

definition
let x be FinSequence of NAT ;
func plus-one x -> Element of NAT equals :: DTCONSTR:def 7
(x . 1) + 1;
coherence
(x . 1) + 1 is Element of NAT
;
end;

:: deftheorem defines plus-one DTCONSTR:def 7 :
for x being FinSequence of NAT holds plus-one x = (x . 1) + 1;

deffunc H3( set , set , FinSequence of NAT ) -> Element of NAT = plus-one $3;

definition
func PN-to-NAT -> Function of (TS PeanoNat),NAT means :Def8: :: DTCONSTR:def 8
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it . (nt -tree ts) = plus-one (it * ts) ) );
existence
ex b1 being Function of (TS PeanoNat),NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) )
proof end;
uniqueness
for b1, b2 being Function of (TS PeanoNat),NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b2 . (nt -tree ts) = plus-one (b2 * ts) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines PN-to-NAT DTCONSTR:def 8 :
for b1 being Function of (TS PeanoNat),NAT holds
( b1 = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) ) );

definition
let x be Element of TS PeanoNat;
func PNsucc x -> Element of TS PeanoNat equals :: DTCONSTR:def 9
1 -tree <*x*>;
coherence
1 -tree <*x*> is Element of TS PeanoNat
proof end;
end;

:: deftheorem defines PNsucc DTCONSTR:def 9 :
for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>;

deffunc H4( set , Element of TS PeanoNat) -> Element of TS PeanoNat = PNsucc $2;

definition
func NAT-to-PN -> Function of NAT,(TS PeanoNat) means :Def10: :: DTCONSTR:def 10
( it . 0 = root-tree 0 & ( for n being Nat holds it . (n + 1) = PNsucc (it . n) ) );
existence
ex b1 being Function of NAT,(TS PeanoNat) st
( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT,(TS PeanoNat) st b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) & b2 . 0 = root-tree 0 & ( for n being Nat holds b2 . (n + 1) = PNsucc (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines NAT-to-PN DTCONSTR:def 10 :
for b1 being Function of NAT,(TS PeanoNat) holds
( b1 = NAT-to-PN iff ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) );

theorem :: DTCONSTR:11
for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)
proof end;

Lm17: 0 = PN-to-NAT . (root-tree O) by Def8
.= PN-to-NAT . (NAT-to-PN . 0) by Def10 ;

Lm18: now :: thesis: for n being Element of NAT st n = PN-to-NAT . (NAT-to-PN . n) holds
n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1))
let n be Element of NAT ; :: thesis: ( n = PN-to-NAT . (NAT-to-PN . n) implies n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) )
assume A1: n = PN-to-NAT . (NAT-to-PN . n) ; :: thesis: n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1))
reconsider dt = NAT-to-PN . n as Element of TS PeanoNat ;
reconsider r = {} as Node of dt by TREES_1:22;
A2: ( dt . r = O or dt . r = S ) by Lm2, TARSKI:def 2;
A3: NAT-to-PN . (n + 1) = PNsucc (NAT-to-PN . n) by Def10
.= S -tree <*(NAT-to-PN . n)*> ;
A4: S ==> roots <*(NAT-to-PN . n)*> by A2, Lm3, Lm4, Th4;
<*(PN-to-NAT . (NAT-to-PN . n))*> = PN-to-NAT * <*(NAT-to-PN . n)*> by FINSEQ_2:35;
then PN-to-NAT . (S -tree <*(NAT-to-PN . n)*>) = plus-one <*n*> by A1, A4, Def8
.= n + 1 by FINSEQ_1:40 ;
hence n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) by A3; :: thesis: verum
end;

theorem :: DTCONSTR:12
for n being Element of NAT holds n = PN-to-NAT . (NAT-to-PN . n)
proof end;

begin

:: Tree traversals and terminal language
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 = {} ;
A2: now :: thesis: for x being set st x in the carrier of G holds
( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) )
let x be set ; :: thesis: ( x in the carrier of G implies ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) ) )
assume x in the carrier of G ; :: thesis: ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) )
hereby :: thesis: ( not S2[x] implies H6(x) in (Terminals G) * )
assume A3: S2[x] ; :: thesis: H5(x) in (Terminals G) *
then reconsider T = Terminals G as non empty set ;
reconsider x9 = x as Element of T by A3;
<*x9*> is FinSequence of T ;
hence H5(x) in (Terminals G) * ; :: thesis: verum
end;
assume not S2[x] ; :: thesis: H6(x) in (Terminals G) *
<*> (Terminals G) = {} ;
hence H6(x) in (Terminals G) * ; :: thesis: verum
end;
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*>;
func TerminalString tsg -> FinSequence of Terminals G means :Def11: :: DTCONSTR:def 11
ex f being Function of (TS G),((Terminals G) *) st
( it = 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) ) );
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) ) )
proof end;
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
proof end;
A17: now :: thesis: for x being set st x in the carrier of G holds
H9(x) in the carrier of G *
let x be set ; :: thesis: ( x in the carrier of G implies H9(x) in the carrier of G * )
assume x in the carrier of G ; :: thesis: H9(x) in the carrier of G *
then reconsider x9 = x as Element of G ;
<*x9*> is FinSequence of the carrier of G ;
hence H9(x) in the carrier of G * ; :: thesis: verum
end;
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);
func PreTraversal tsg -> FinSequence of the carrier of G means :Def12: :: DTCONSTR:def 12
ex f being Function of (TS G),( the carrier of G *) st
( it = 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) ) );
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) ) )
proof end;
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
proof end;
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);
func PostTraversal tsg -> FinSequence of the carrier of G means :Def13: :: DTCONSTR:def 13
ex f being Function of (TS G),( the carrier of G *) st
( it = 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*> ) );
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*> ) )
proof end;
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
proof end;
end;

:: deftheorem Def11 defines TerminalString DTCONSTR:def 11 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of Terminals G holds
( b3 = TerminalString tsg iff ex f being Function of (TS G),((Terminals G) *) st
( b3 = 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) ) ) );

:: deftheorem Def12 defines PreTraversal DTCONSTR:def 12 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PreTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st
( b3 = 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) ) ) );

:: deftheorem Def13 defines PostTraversal DTCONSTR:def 13 :
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PostTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st
( b3 = 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*> ) ) );

definition
let G be non empty with_nonterminals DTConstrStr ;
let nt be Symbol of G;
func TerminalLanguage nt -> Subset of ((Terminals G) *) equals :: DTCONSTR:def 14
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *)
proof end;
func PreTraversalLanguage nt -> Subset of ( the carrier of G *) equals :: DTCONSTR:def 15
{ (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *)
proof end;
func PostTraversalLanguage nt -> Subset of ( the carrier of G *) equals :: DTCONSTR:def 16
{ (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *)
proof end;
end;

:: deftheorem defines TerminalLanguage DTCONSTR:def 14 :
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds TerminalLanguage nt = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;

:: deftheorem defines PreTraversalLanguage DTCONSTR:def 15 :
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds PreTraversalLanguage nt = { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;

:: deftheorem defines PostTraversalLanguage DTCONSTR:def 16 :
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds PostTraversalLanguage nt = { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;

theorem Th13: :: DTCONSTR:13
for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
TerminalString t = <*0*>
proof end;

theorem :: DTCONSTR:14
for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}
proof end;

theorem Th15: :: DTCONSTR:15
for t being Element of TS PeanoNat holds PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
proof end;

theorem :: DTCONSTR:16
for nt being Symbol of PeanoNat holds
( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) )
proof end;

theorem Th17: :: DTCONSTR:17
for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
proof end;

theorem :: DTCONSTR:18
for nt being Symbol of PeanoNat holds
( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) )
proof end;