:: 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
proofend;

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
proofend;

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
proofend;
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
proofend;
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 . {})*>
proofend;

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*> &amp; x in F )
proofend;

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

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
proofend;
:: original:pr2
redefine func pr2 f ->  FinSequence of Y;
coherence
 pr2 f is FinSequence of Y
proofend;
end;

theorem Th7: :: DTCONSTR:7
( pr1 {} = {} &amp; pr2 {} = {} )
proofend;

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() &amp; ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P1[x,p] ) ) )
proofend;

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() &amp; ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] ) ) &amp; the carrier of G2 = F1() &amp; ( 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
proofend;

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

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() &amp; ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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() &amp; d = F4(t) ) or ( t ==> {} &amp; 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 &amp; o ==> pr1 (roots q) )  }
proofend;

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()  }  &amp; ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) &amp; ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) &amp; ( 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 ) &amp; ( 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() &amp; d = F4(t) ) or ( t ==> {} &amp; 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 &amp; o ==> pr1 (roots q) )  }
proofend;

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() &amp; d = F4(t) ) or ( t ==> {} &amp; 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 &amp; o ==> pr1 (roots q) )  }
proofend;

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() &amp; dt2 in Union F1() &amp; 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() &amp; d = F4(t) ) or ( t ==> {} &amp; 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 &amp; o ==> pr1 (roots q) )  }
proofend;

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 ) &amp; ( for o being Symbol of G
for p being FinSequence of it st o ==> roots p holds
o -tree p in it ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) &amp; ( 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 ) &amp; ( 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 ) )
proofend;
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 ) &amp; ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) &amp; ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) &amp; ( 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 ) &amp; ( 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
proofend;
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 ) &amp; ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) &amp; ( 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 ) &amp; ( 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 &amp; ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proofend;

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) ) &amp; ( 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)) ) )
proofend;

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) ) &amp; ( 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) ) &amp; ( 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)) ) )
proofend;

begin

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

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

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}
proofend;

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 ;
attrG is with_terminals  means :Def3: :: DTCONSTR:def 3
 Terminals G <> {} ;
attrG is with_nonterminals  means :Def4: :: DTCONSTR:def 4
 NonTerminals G <> {} ;
attrG 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 &amp; PeanoNat is with_nonterminals &amp; PeanoNat is with_useful_nonterminals )
proofend;

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 &amp; b1 is with_nonterminals &amp; b1 is with_useful_nonterminals &amp; 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
proofend;
end;

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

registration
let G be non empty with_useful_nonterminals DTConstrStr ;
cluster TS G ->  non empty ;
coherence
 not TS G is empty
proofend;
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
proofend;
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 funcnt -tree p ->  Element of TS G;
coherence
 nt -tree p is Element of TS G
proofend;
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
proofend;

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 &amp; nt ==> roots ts )
proofend;

begin

:: Peano naturals continued
registration
cluster PeanoNat  ->  non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
 ( PeanoNat is with_terminals &amp; PeanoNat is with_nonterminals &amp; 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 funcnt -tree t ->  Element of TS PeanoNat;
coherence
 nt -tree t is Element of TS PeanoNat
proofend;
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 ) &amp; ( 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 ) &amp; ( 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) ) )
proofend;
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 ) &amp; ( 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) ) &amp; ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b2 . (root-tree t) = 0 ) &amp; ( 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
proofend;
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 ) &amp; ( 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
proofend;
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 &amp; ( 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 &amp; ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(TS PeanoNat) st b1 . 0 = root-tree 0 &amp; ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) &amp; b2 . 0 = root-tree 0 &amp; ( for n being Nat holds b2 . (n + 1) = PNsucc (b2 . n) ) holds
b1 = b2
proofend;
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 &amp; ( 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)
proofend;

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)
proofend;

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)_*_)_&amp;_(_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) * ) &amp; ( 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) * ) &amp; ( 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) ) &amp; ( 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( 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) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of Terminals G st ex f being Function of (TS G),((Terminals G) *) st
( b1 = f . tsg &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( 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) ) ) &amp; ex f being Function of (TS G),((Terminals G) *) st
( b2 = f . tsg &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( 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
proofend;
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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) )
proofend;
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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) &amp; ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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
proofend;
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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
proofend;
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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) &amp; ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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
proofend;
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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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 &amp; ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) &amp; ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts &amp; 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 &amp; tsg . {} = nt )  }  ;
coherence
  {  (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G &amp; tsg . {} = nt )  }  is Subset of ((Terminals G) *)
proofend;
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 &amp; tsg . {} = nt )  }  ;
coherence
  {  (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G &amp; tsg . {} = nt )  }  is Subset of ( the carrier of G *)
proofend;
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 &amp; tsg . {} = nt )  }  ;
coherence
  {  (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G &amp; tsg . {} = nt )  }  is Subset of ( the carrier of G *)
proofend;
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 &amp; 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 &amp; 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 &amp; tsg . {} = nt )  }  ;

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

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

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

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

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

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