:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received October 12, 1993

:: Copyright (c) 1993-2012 Association of Mizar Users

begin

deffunc H

deffunc H

registration

let D be non empty set ;

let T be DTree-set of D;

coherence

for b_{1} being FinSequence of T holds b_{1} is DTree-yielding
;

end;
let T be DTree-set of D;

coherence

for b

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 b_{1} being Element of Tset holds b_{1} is Element of F

end;
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 b

proof 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

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

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

.= {} ;

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 )

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;

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

redefine func pr2 f -> FinSequence of Y;

coherence

pr2 f is FinSequence of Y

end;
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: pr2redefine func pr2 f -> FinSequence of Y;

coherence

pr2 f is FinSequence of Y

proof end;

begin

registration
end;

scheme :: DTCONSTR:sch 1

DTConstrStrEx{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

DTConstrStrEx{ F

ex G being non empty strict DTConstrStr st

( the carrier of G = F_{1}() & ( for x being Symbol of G

for p being FinSequence of the carrier of G holds

( x ==> p iff P_{1}[x,p] ) ) )

( the carrier of G = F

for p being FinSequence of the carrier of G holds

( x ==> p iff P

proof end;

scheme :: DTCONSTR:sch 2

DTConstrStrUniq{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

DTConstrStrUniq{ F

for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = F_{1}() & ( for x being Symbol of G1

for p being FinSequence of the carrier of G1 holds

( x ==> p iff P_{1}[x,p] ) ) & the carrier of G2 = F_{1}() & ( for x being Symbol of G2

for p being FinSequence of the carrier of G2 holds

( x ==> p iff P_{1}[x,p] ) ) holds

G1 = G2

for p being FinSequence of the carrier of G1 holds

( x ==> p iff P

for p being FinSequence of the carrier of G2 holds

( x ==> p iff P

G1 = G2

proof end;

scheme :: DTCONSTR:sch 3

DTCMin{ F_{1}() -> Function, F_{2}() -> non empty DTConstrStr , F_{3}() -> non empty set , F_{4}( set ) -> Element of F_{3}(), F_{5}( set , set , set ) -> Element of F_{3}() } :

DTCMin{ F

ex X being Subset of (FinTrees [: the carrier of F_{2}(),F_{3}():]) st

( X = Union F_{1}() & ( for d being Symbol of F_{2}() st d in Terminals F_{2}() holds

root-tree [d,F_{4}(d)] in X ) & ( for o being Symbol of F_{2}()

for p being FinSequence of X st o ==> pr1 (roots p) holds

[o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F_{2}(),F_{3}():]) st ( for d being Symbol of F_{2}() st d in Terminals F_{2}() holds

root-tree [d,F_{4}(d)] in F ) & ( for o being Symbol of F_{2}()

for p being FinSequence of F st o ==> pr1 (roots p) holds

[o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds

X c= F ) )

provided( X = Union F

root-tree [d,F

for p being FinSequence of X st o ==> pr1 (roots p) holds

[o,F

root-tree [d,F

for p being FinSequence of F st o ==> pr1 (roots p) holds

[o,F

X c= F ) )

A1:
dom F_{1}() = NAT
and

A2: F_{1}() . 0 = { (root-tree [t,d]) where t is Symbol of F_{2}(), d is Element of F_{3}() : ( ( t in Terminals F_{2}() & d = F_{4}(t) ) or ( t ==> {} & d = F_{5}(t,{},{}) ) ) }
and

A3: for n being Element of NAT holds F_{1}() . (n + 1) = (F_{1}() . n) \/ { ([o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F_{2}(), p is Element of (F_{1}() . n) * : ex q being FinSequence of FinTrees [: the carrier of F_{2}(),F_{3}():] st

( p = q & o ==> pr1 (roots q) ) }

A2: F

A3: for n being Element of NAT holds F

( p = q & o ==> pr1 (roots q) ) }

proof end;

scheme :: DTCONSTR:sch 4

DTCSymbols{ F_{1}() -> Function, F_{2}() -> non empty DTConstrStr , F_{3}() -> non empty set , F_{4}( set ) -> Element of F_{3}(), F_{5}( set , set , set ) -> Element of F_{3}() } :

DTCSymbols{ F

ex X1 being Subset of (FinTrees the carrier of F_{2}()) st

( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F_{2}(),F_{3}():] : t in Union F_{1}() } & ( for d being Symbol of F_{2}() st d in Terminals F_{2}() holds

root-tree d in X1 ) & ( for o being Symbol of F_{2}()

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 F_{2}()) st ( for d being Symbol of F_{2}() st d in Terminals F_{2}() holds

root-tree d in F ) & ( for o being Symbol of F_{2}()

for p being FinSequence of F st o ==> roots p holds

o -tree p in F ) holds

X1 c= F ) )

provided( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F

root-tree d in X1 ) & ( for o being Symbol of F

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 F

root-tree d in F ) & ( for o being Symbol of F

for p being FinSequence of F st o ==> roots p holds

o -tree p in F ) holds

X1 c= F ) )

A1:
dom F_{1}() = NAT
and

A2: F_{1}() . 0 = { (root-tree [t,d]) where t is Symbol of F_{2}(), d is Element of F_{3}() : ( ( t in Terminals F_{2}() & d = F_{4}(t) ) or ( t ==> {} & d = F_{5}(t,{},{}) ) ) }
and

A3: for n being Element of NAT holds F_{1}() . (n + 1) = (F_{1}() . n) \/ { ([o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F_{2}(), p is Element of (F_{1}() . n) * : ex q being FinSequence of FinTrees [: the carrier of F_{2}(),F_{3}():] st

( p = q & o ==> pr1 (roots q) ) }

A2: F

A3: for n being Element of NAT holds F

( p = q & o ==> pr1 (roots q) ) }

proof end;

scheme :: DTCONSTR:sch 5

DTCHeight{ F_{1}() -> Function, F_{2}() -> non empty DTConstrStr , F_{3}() -> non empty set , F_{4}( set ) -> Element of F_{3}(), F_{5}( set , set , set ) -> Element of F_{3}() } :

DTCHeight{ F

for n being Element of NAT

for dt being Element of FinTrees [: the carrier of F_{2}(),F_{3}():] st dt in Union F_{1}() holds

( dt in F_{1}() . n iff height (dom dt) <= n )

providedfor dt being Element of FinTrees [: the carrier of F

( dt in F

A1:
dom F_{1}() = NAT
and

A2: F_{1}() . 0 = { (root-tree [t,d]) where t is Symbol of F_{2}(), d is Element of F_{3}() : ( ( t in Terminals F_{2}() & d = F_{4}(t) ) or ( t ==> {} & d = F_{5}(t,{},{}) ) ) }
and

A3: for n being Element of NAT holds F_{1}() . (n + 1) = (F_{1}() . n) \/ { ([o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F_{2}(), p is Element of (F_{1}() . n) * : ex q being FinSequence of FinTrees [: the carrier of F_{2}(),F_{3}():] st

( p = q & o ==> pr1 (roots q) ) }

A2: F

A3: for n being Element of NAT holds F

( p = q & o ==> pr1 (roots q) ) }

proof end;

scheme :: DTCONSTR:sch 6

DTCUniq{ F_{1}() -> Function, F_{2}() -> non empty DTConstrStr , F_{3}() -> non empty set , F_{4}( set ) -> Element of F_{3}(), F_{5}( set , set , set ) -> Element of F_{3}() } :

A1:
dom F_{1}() = NAT
and

A2: F_{1}() . 0 = { (root-tree [t,d]) where t is Symbol of F_{2}(), d is Element of F_{3}() : ( ( t in Terminals F_{2}() & d = F_{4}(t) ) or ( t ==> {} & d = F_{5}(t,{},{}) ) ) }
and

A3: for n being Element of NAT holds F_{1}() . (n + 1) = (F_{1}() . n) \/ { ([o,F_{5}(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F_{2}(), p is Element of (F_{1}() . n) * : ex q being FinSequence of FinTrees [: the carrier of F_{2}(),F_{3}():] st

( p = q & o ==> pr1 (roots q) ) }

DTCUniq{ F

for dt1, dt2 being DecoratedTree of [: the carrier of F_{2}(),F_{3}():] st dt1 in Union F_{1}() & dt2 in Union F_{1}() & dt1 `1 = dt2 `1 holds

dt1 = dt2

provideddt1 = dt2

A2: F

A3: for n being Element of NAT holds F

( p = q & o ==> pr1 (roots q) ) }

proof end;

definition

let G be non empty DTConstrStr ;

ex b_{1} 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 b_{1} ) & ( for o being Symbol of G

for p being FinSequence of b_{1} st o ==> roots p holds

o -tree p in b_{1} ) & ( 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

b_{1} c= F ) )

for b_{1}, b_{2} 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 b_{1} ) & ( for o being Symbol of G

for p being FinSequence of b_{1} st o ==> roots p holds

o -tree p in b_{1} ) & ( 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

b_{1} c= F ) & ( for d being Symbol of G st d in Terminals G holds

root-tree d in b_{2} ) & ( for o being Symbol of G

for p being FinSequence of b_{2} st o ==> roots p holds

o -tree p in b_{2} ) & ( 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

b_{2} c= F ) holds

b_{1} = b_{2}

end;
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 ( ( 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 ) );

ex b

( ( for d being Symbol of G st d in Terminals G holds

root-tree d in b

for p being FinSequence of b

o -tree p in b

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

b

proof end;

uniqueness for b

root-tree d in b

for p being FinSequence of b

o -tree p in b

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

b

root-tree d in b

for p being FinSequence of b

o -tree p in b

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

b

b

proof end;

:: deftheorem Def1 defines TS DTCONSTR:def 1 :

for G being non empty DTConstrStr

for b_{2} being Subset of (FinTrees the carrier of G) holds

( b_{2} = TS G iff ( ( for d being Symbol of G st d in Terminals G holds

root-tree d in b_{2} ) & ( for o being Symbol of G

for p being FinSequence of b_{2} st o ==> roots p holds

o -tree p in b_{2} ) & ( 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

b_{2} c= F ) ) );

for G being non empty DTConstrStr

for b

( b

root-tree d in b

for p being FinSequence of b

o -tree p in b

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

b

scheme :: DTCONSTR:sch 7

DTConstrInd{ F_{1}() -> non empty DTConstrStr , P_{1}[ set ] } :

provided

DTConstrInd{ F

provided

A1:
for s being Symbol of F_{1}() st s in Terminals F_{1}() holds

P_{1}[ root-tree s]
and

A2: for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F_{1}() st t in rng ts holds

P_{1}[t] ) holds

P_{1}[nt -tree ts]

P

A2: for nt being Symbol of F

for ts being FinSequence of TS F

P

P

proof end;

scheme :: DTCONSTR:sch 8

DTConstrIndDef{ F_{1}() -> non empty DTConstrStr , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}( set , set , set ) -> Element of F_{2}() } :

DTConstrIndDef{ F

ex f being Function of (TS F_{1}()),F_{2}() st

( ( for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

f . (root-tree t) = F_{3}(t) ) & ( for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

f . (nt -tree ts) = F_{4}(nt,(roots ts),(f * ts)) ) )

( ( for t being Symbol of F

f . (root-tree t) = F

for ts being FinSequence of TS F

f . (nt -tree ts) = F

proof end;

scheme :: DTCONSTR:sch 9

DTConstrUniqDef{ F_{1}() -> non empty DTConstrStr , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}( set , set , set ) -> Element of F_{2}(), F_{5}() -> Function of (TS F_{1}()),F_{2}(), F_{6}() -> Function of (TS F_{1}()),F_{2}() } :

provided

DTConstrUniqDef{ F

provided

A1:
( ( for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{5}() . (root-tree t) = F_{3}(t) ) & ( for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{5}() . (nt -tree ts) = F_{4}(nt,(roots ts),(F_{5}() * ts)) ) )
and

A2: ( ( for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{6}() . (root-tree t) = F_{3}(t) ) & ( for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{6}() . (nt -tree ts) = F_{4}(nt,(roots ts),(F_{6}() * ts)) ) )

F

for ts being FinSequence of TS F

F

A2: ( ( for t being Symbol of F

F

for ts being FinSequence of TS F

F

proof end;

begin

defpred S

definition

ex b_{1} being non empty strict DTConstrStr st

( the carrier of b_{1} = {0,1} & ( for x being Symbol of b_{1}

for y being FinSequence of the carrier of b_{1} holds

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) )

for b_{1}, b_{2} being non empty strict DTConstrStr st the carrier of b_{1} = {0,1} & ( for x being Symbol of b_{1}

for y being FinSequence of the carrier of b_{1} holds

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) & the carrier of b_{2} = {0,1} & ( for x being Symbol of b_{2}

for y being FinSequence of the carrier of b_{2} holds

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) holds

b_{1} = b_{2}
end;

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

ex b

( the carrier of b

for y being FinSequence of the carrier of b

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) )

proof end;

uniqueness for b

for y being FinSequence of the carrier of b

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) & the carrier of b

for y being FinSequence of the carrier of b

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines PeanoNat DTCONSTR:def 2 :

for b_{1} being non empty strict DTConstrStr holds

( b_{1} = PeanoNat iff ( the carrier of b_{1} = {0,1} & ( for x being Symbol of b_{1}

for y being FinSequence of the carrier of b_{1} holds

( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ) );

for b

( b

for y being FinSequence of the carrier of b

( 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;
[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

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 ;

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

for nt being Symbol of G st nt in NonTerminals G holds

ex p being FinSequence of TS G st nt ==> roots p;

:: deftheorem Def3 defines with_terminals DTCONSTR:def 3 :

for G being non empty DTConstrStr holds

( G is with_terminals iff Terminals G <> {} );

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

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

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

ex b_{1} being non empty DTConstrStr st

( b_{1} is with_terminals & b_{1} is with_nonterminals & b_{1} is with_useful_nonterminals & b_{1} is strict )
by Lm16;

end;

cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals for DTConstrStr ;

existence ex b

( b

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

end;
:: original: Terminals

redefine func Terminals G -> non empty Subset of G;

coherence

Terminals G is non empty Subset of G

proof end;

registration
end;

registration
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

end;
:: original: NonTerminals

redefine func NonTerminals G -> non empty Subset of G;

coherence

NonTerminals G is non empty Subset of G

proof end;

definition
end;

definition

let G be non empty with_nonterminals DTConstrStr ;

mode NonTerminal of G is Element of NonTerminals G;

end;
mode NonTerminal of G is Element of NonTerminals G;

definition

let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;

let nt be NonTerminal of G;

existence

ex b_{1} being FinSequence of TS G st nt ==> roots b_{1}
by Def5;

end;
let nt be NonTerminal of G;

existence

ex b

:: 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 b_{3} being FinSequence of TS G holds

( b_{3} is SubtreeSeq of nt iff nt ==> roots b_{3} );

for G being non empty with_nonterminals with_useful_nonterminals DTConstrStr

for nt being NonTerminal of G

for b

( b

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

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

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

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

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 )

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

coherence

( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) by Lm16;

end;
( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) by Lm16;

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

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

:: deftheorem defines plus-one DTCONSTR:def 7 :

for x being FinSequence of NAT holds plus-one x = (x . 1) + 1;

for x being FinSequence of NAT holds plus-one x = (x . 1) + 1;

deffunc H

definition

ex b_{1} being Function of (TS PeanoNat),NAT st

( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds

b_{1} . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b_{1} . (nt -tree ts) = plus-one (b_{1} * ts) ) )

for b_{1}, b_{2} being Function of (TS PeanoNat),NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds

b_{1} . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b_{1} . (nt -tree ts) = plus-one (b_{1} * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds

b_{2} . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b_{2} . (nt -tree ts) = plus-one (b_{2} * ts) ) holds

b_{1} = b_{2}
end;

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

ex b

( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds

b

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b

proof end;

uniqueness for b

b

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b

b

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b

b

proof end;

:: deftheorem Def8 defines PN-to-NAT DTCONSTR:def 8 :

for b_{1} being Function of (TS PeanoNat),NAT holds

( b_{1} = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds

b_{1} . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b_{1} . (nt -tree ts) = plus-one (b_{1} * ts) ) ) );

for b

( b

b

for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds

b

definition
end;

:: deftheorem defines PNsucc DTCONSTR:def 9 :

for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>;

for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>;

deffunc H

definition

ex b_{1} being Function of NAT,(TS PeanoNat) st

( b_{1} . 0 = root-tree 0 & ( for n being Nat holds b_{1} . (n + 1) = PNsucc (b_{1} . n) ) )

for b_{1}, b_{2} being Function of NAT,(TS PeanoNat) st b_{1} . 0 = root-tree 0 & ( for n being Nat holds b_{1} . (n + 1) = PNsucc (b_{1} . n) ) & b_{2} . 0 = root-tree 0 & ( for n being Nat holds b_{2} . (n + 1) = PNsucc (b_{2} . n) ) holds

b_{1} = b_{2}
end;

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 ( it . 0 = root-tree 0 & ( for n being Nat holds it . (n + 1) = PNsucc (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines NAT-to-PN DTCONSTR:def 10 :

for b_{1} being Function of NAT,(TS PeanoNat) holds

( b_{1} = NAT-to-PN iff ( b_{1} . 0 = root-tree 0 & ( for n being Nat holds b_{1} . (n + 1) = PNsucc (b_{1} . n) ) ) );

for b

( b

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

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

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 S_{2}[ set ] means $1 in Terminals G;

deffunc H_{5}( set ) -> set = <*$1*>;

deffunc H_{6}( set ) -> set = {} ;

A4: for s being set st s in the carrier of G holds

( ( S_{2}[s] implies s2t . s = H_{5}(s) ) & ( not S_{2}[s] implies s2t . s = H_{6}(s) ) )
from FUNCT_2:sch 5(A2);

deffunc H_{7}( Symbol of G) -> Element of (Terminals G) * = s2t . $1;

deffunc H_{8}( set , set , FinSequence of (Terminals G) * ) -> Element of (Terminals G) * = FlattenSeq $3;

deffunc H_{9}( set ) -> set = <*$1*>;

ex b_{1} being FinSequence of Terminals G ex f being Function of (TS G),((Terminals G) *) st

( b_{1} = 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) ) )

for b_{1}, b_{2} being FinSequence of Terminals G st ex f being Function of (TS G),((Terminals G) *) st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

A18: for s being set st s in the carrier of G holds

s2s . s = H_{9}(s)
from FUNCT_2:sch 2(A17);

deffunc H_{10}( Symbol of G) -> Element of the carrier of G * = s2s . $1;

deffunc H_{11}( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3);

ex b_{1} being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st

( b_{1} = 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) ) )

for b_{1}, b_{2} being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}
_{12}( Symbol of G) -> Element of the carrier of G * = s2s . $1;

deffunc H_{13}( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (FlattenSeq $3) ^ (s2s . $1);

ex b_{1} being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st

( b_{1} = 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*> ) )

for b_{1}, b_{2} being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
let tsg be DecoratedTree of the carrier of G;

assume A1: tsg in TS G ;

defpred S

deffunc H

deffunc H

A2: now :: thesis: for x being set st x in the carrier of G holds

( ( S_{2}[x] implies H_{5}(x) in (Terminals G) * ) & ( not S_{2}[x] implies H_{6}(x) in (Terminals G) * ) )

consider s2t being Function of the carrier of G,((Terminals G) *) such that ( ( S

let x be set ; :: thesis: ( x in the carrier of G implies ( ( S_{2}[x] implies H_{5}(x) in (Terminals G) * ) & ( not S_{2}[x] implies H_{6}(x) in (Terminals G) * ) ) )

assume x in the carrier of G ; :: thesis: ( ( S_{2}[x] implies H_{5}(x) in (Terminals G) * ) & ( not S_{2}[x] implies H_{6}(x) in (Terminals G) * ) )

_{2}[x]
; :: thesis: H_{6}(x) in (Terminals G) *

<*> (Terminals G) = {} ;

hence H_{6}(x) in (Terminals G) *
; :: thesis: verum

end;
assume x in the carrier of G ; :: thesis: ( ( S

hereby :: thesis: ( not S_{2}[x] implies H_{6}(x) in (Terminals G) * )

assume
not S
assume A3:
S_{2}[x]
; :: thesis: H_{5}(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 H_{5}(x) in (Terminals G) *
; :: thesis: verum

end;
then reconsider T = Terminals G as non empty set ;

reconsider x9 = x as Element of T by A3;

<*x9*> is FinSequence of T ;

hence H

<*> (Terminals G) = {} ;

hence H

A4: for s being set st s in the carrier of G holds

( ( S

deffunc H

deffunc H

deffunc H

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

ex b

( b

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 b

( b

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

( b

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

b

proof end;

A17: now :: thesis: for x being set st x in the carrier of G holds

H_{9}(x) in the carrier of G *

consider s2s being Function of the carrier of G,( the carrier of G *) such that H

let x be set ; :: thesis: ( x in the carrier of G implies H_{9}(x) in the carrier of G * )

assume x in the carrier of G ; :: thesis: H_{9}(x) in the carrier of G *

then reconsider x9 = x as Element of G ;

<*x9*> is FinSequence of the carrier of G ;

hence H_{9}(x) in the carrier of G *
; :: thesis: verum

end;
assume x in the carrier of G ; :: thesis: H

then reconsider x9 = x as Element of G ;

<*x9*> is FinSequence of the carrier of G ;

hence H

A18: for s being set st s in the carrier of G holds

s2s . s = H

deffunc H

deffunc H

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

ex b

( b

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 b

( b

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

( b

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

b

proof end;

deffunc Hdeffunc H

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

ex b

( b

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 b

( b

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

( b

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

b

proof 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 b_{3} being FinSequence of Terminals G holds

( b_{3} = TerminalString tsg iff ex f being Function of (TS G),((Terminals G) *) st

( b_{3} = 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) ) ) );

for G being non empty DTConstrStr

for tsg being DecoratedTree of the carrier of G st tsg in TS G holds

for b

( b

( b

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 b_{3} being FinSequence of the carrier of G holds

( b_{3} = PreTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st

( b_{3} = 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) ) ) );

for G being non empty DTConstrStr

for tsg being DecoratedTree of the carrier of G st tsg in TS G holds

for b

( b

( b

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 b_{3} being FinSequence of the carrier of G holds

( b_{3} = PostTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st

( b_{3} = 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*> ) ) );

for G being non empty DTConstrStr

for tsg being DecoratedTree of the carrier of G st tsg in TS G holds

for b

( b

( b

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;

{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *)

{ (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 *)

{ (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 *)

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

{ (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 ) } ;

{ (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 ) } ;

{ (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;

:: 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 ) } ;

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

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

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*>

TerminalString t = <*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 } ) )

( ( 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 :: 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 } ) )

( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) )

proof end;