:: On Defining Functions on Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Copyright (c) 1993-2021 Association of Mizar Users

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 () = dom {} by TREES_3:def 18
.= {} ;

theorem Th3: :: DTCONSTR:3

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 ()
for p being FinSequence of F st len () = 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
proof end;

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[ object , object ] } :
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 () holds
[o,F5(o,(pr1 ()),(pr2 ()))] -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 () holds
[o,F5(o,(pr1 ()),(pr2 ()))] -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 Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 ()),(pr2 ()))] -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 () )
}
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 Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 ()),(pr2 ()))] -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 () )
}
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 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 Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 ()),(pr2 ()))] -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 () )
}
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 Nat holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 ()),(pr2 ()))] -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 () )
}
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
;
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 . () = 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() . () = 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() . () = 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;

defpred S1[ set , set ] means ( $1 = 1 & ($2 = 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 = 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 = 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 = 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 = 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 = 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 ; 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 ; :: thesis: verum end; then Lm9: by Lm7; Lm10: 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: by Lm5; then Lm13: by ZFMISC_1:31; Lm14: proof end; then Lm15: by Lm13; reconsider TSPN = TS PeanoNat as non empty Subset of () by ; :: 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: proof end; registration 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 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; :: Peano naturals continued registration coherence 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 (),NAT means :Def8: :: DTCONSTR:def 8
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it . () = 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 (),NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . () = 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 (),NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . () = 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 . () = 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 (),NAT holds
( b1 = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . () = 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
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 -> sequence of () 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 sequence of () st ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) proof end; uniqueness for b1, b2 being sequence of () 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 sequence of () 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 . () proof end; Lm17: 0 = PN-to-NAT . () by Def8 .= PN-to-NAT . () by Def10 ; Lm18: now :: thesis: for n being Element of NAT st n = PN-to-NAT . () holds n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) let n be Element of NAT ; :: thesis: ( n = PN-to-NAT . () implies n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) ) assume A1: n = PN-to-NAT . () ; :: 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 ; A3: NAT-to-PN . (n + 1) = PNsucc () by Def10 .= S -tree <*()*> ; A4: S ==> roots <*()*> by A2, Lm3, Lm4, Th4; <*(PN-to-NAT . ())*> = PN-to-NAT * <*()*> by FINSEQ_2:35; then PN-to-NAT . (S -tree <*()*>) = 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 Nat holds n = PN-to-NAT . () proof end; :: 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[ object ] means$1 in Terminals G;
deffunc H5( object ) -> set = <*$1*>; deffunc H6( object ) -> set = {} ; A2: now :: thesis: for x being object st x in the carrier of G holds ( ( S2[x] implies H5(x) in () * ) & ( not S2[x] implies H6(x) in () * ) ) let x be object ; :: thesis: ( x in the carrier of G implies ( ( S2[x] implies H5(x) in () * ) & ( not S2[x] implies H6(x) in () * ) ) ) assume x in the carrier of G ; :: thesis: ( ( S2[x] implies H5(x) in () * ) & ( not S2[x] implies H6(x) in () * ) ) hereby :: thesis: ( not S2[x] implies H6(x) in () * ) assume A3: S2[x] ; :: thesis: H5(x) in () * 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 () * ; :: thesis: verum end; assume not S2[x] ; :: thesis: H6(x) in () * <*> () = {} ; hence H6(x) in () * ; :: thesis: verum end; consider s2t being Function of the carrier of G,(() *) such that A4: for s being object st s in the carrier of G holds ( ( S2[s] implies s2t . s = H5(s) ) & ( not S2[s] implies s2t . s = H6(s) ) ) from deffunc H7( Symbol of G) -> Element of () * = s2t .$1;
deffunc H8( set , set , FinSequence of () * ) -> Element of () * = FlattenSeq $3; deffunc H9( object ) -> set = <*$1*>;
func TerminalString tsg -> FinSequence of Terminals G means :Def11: :: DTCONSTR:def 11
ex f being Function of (TS G),(() *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . () = <*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),(() *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . () = <*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),(() *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . () = <*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),(() *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . () = <*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 object st x in the carrier of G holds
H9(x) in the carrier of G *
let x be object ; :: 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 object st s in the carrier of G holds
s2s . s = H9(s) from 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) ^ ();
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 . () = <*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*> ^ () ) );
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 . () = <*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*> ^ () ) )
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 . () = <*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*> ^ () ) ) & 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 . () = <*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*> ^ () ) ) 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 * = () ^ (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 . () = <*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*> ) );
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 . () = <*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*> ) )
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 . () = <*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*> ) ) & 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 . () = <*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*> ) ) 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),(() *) st
( b3 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . () = <*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 . () = <*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*> ^ () ) ) );

:: 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 . () = <*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*> ) ) );

definition
let G be non empty with_nonterminals DTConstrStr ;
let nt be Symbol of G;
func TerminalLanguage nt -> Subset of (() *) equals :: DTCONSTR:def 14
{ () where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ () where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of (() *)
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
{ () where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ () 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 = { () 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 = { () 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 =
proof end;

theorem :: DTCONSTR:14
for nt being Symbol of PeanoNat holds TerminalLanguage nt =
proof end;

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

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

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

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