DTCONSTR: On Defining Functions on Trees

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 ;

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

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

proof end;

end;

theorem Th3: :: DTCONSTR:3

roots {} = {} by Lm1;

theorem Th4: :: DTCONSTR:4

for T being DecoratedTree holds roots <*T*> = <*(T . {})*>

proof end;

theorem Th5: :: DTCONSTR:5

for D being non empty set
for F being Subset of (FinTrees D)
for p being FinSequence of F st len (roots p) = 1 holds
ex x being Element of FinTrees D st
( p = <*x*> & x in F )

proof end;

theorem :: DTCONSTR:6

for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>

proof end;

definition

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

proof end;

:: original: pr2
redefine func pr2 f -> FinSequence of Y;
coherence

proof end;

end;

theorem Th7: :: DTCONSTR:7

( pr1 {} = {} & pr2 {} = {} )

proof end;

registration

let A be non empty set ;
let R be Relation of A,(A *);

cluster DTConstrStr(# A,R #) -> non empty ;

coherence ;

end;

scheme :: DTCONSTR:sch 1
DTConstrStrEx{ F₁() -> non empty set , P₁[ object , object ] } :

ex G being non empty strict DTConstrStr st
( the carrier of G = F₁() & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P₁[x,p] ) ) )

proof end;

scheme :: DTCONSTR:sch 2
DTConstrStrUniq{ F₁() -> non empty set , P₁[ set , set ] } :

for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = F₁() & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P₁[x,p] ) ) & the carrier of G2 = F₁() & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P₁[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{ F₁() -> Function, F₂() -> non empty DTConstrStr , F₃() -> non empty set , F₄( set ) -> Element of F₃(), F₅( set , set , set ) -> Element of F₃() } :

ex X being Subset of (FinTrees [: the carrier of F₂(),F₃():]) st
( X = Union F₁() & ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in X ) & ( for o being Symbol of F₂()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F₂(),F₃():]) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )

provided

A1: dom F₁() = NAT and
A2: F₁() . 0 = { (root-tree [t,d]) where t is Symbol of F₂(), d is Element of F₃() : ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(t,{},{}) ) ) } and
A3: for n being Nat holds F₁() . (n + 1) = (F₁() . n) \/ { ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) }

proof end;

scheme :: DTCONSTR:sch 4
DTCSymbols{ F₁() -> Function, F₂() -> non empty DTConstrStr , F₃() -> non empty set , F₄( set ) -> Element of F₃(), F₅( set , set , set ) -> Element of F₃() } :

ex X1 being Subset of (FinTrees the carrier of F₂()) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F₂(),F₃():] : t in Union F₁() } & ( for d being Symbol of F₂() st d in Terminals F₂() holds
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₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
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 ) )

provided

proof end;

scheme :: DTCONSTR:sch 5
DTCHeight{ F₁() -> Function, F₂() -> non empty DTConstrStr , F₃() -> non empty set , F₄( set ) -> Element of F₃(), F₅( set , set , set ) -> Element of F₃() } :

for n being Nat
for dt being Element of FinTrees [: the carrier of F₂(),F₃():] st dt in Union F₁() holds
( dt in F₁() . n iff height (dom dt) <= n )

provided

proof end;

scheme :: DTCONSTR:sch 6
DTCUniq{ F₁() -> Function, F₂() -> non empty DTConstrStr , F₃() -> non empty set , F₄( set ) -> Element of F₃(), F₅( set , set , set ) -> Element of F₃() } :

for dt1, dt2 being DecoratedTree of [: the carrier of F₂(),F₃():] st dt1 in Union F₁() & dt2 in Union F₁() & dt1 `1 = dt2 `1 holds
dt1 = dt2

provided

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

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines TS DTCONSTR:def 1 :

scheme :: DTCONSTR:sch 7
DTConstrInd{ F₁() -> non empty DTConstrStr , P₁[ set ] } :

for t being DecoratedTree of the carrier of F₁() st t in TS F₁() holds
P₁[t]

provided

A1: for s being Symbol of F₁() st s in Terminals F₁() holds
P₁[ root-tree s] and
A2: for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F₁() st t in rng ts holds
P₁[t] ) holds
P₁[nt -tree ts]

proof end;

scheme :: DTCONSTR:sch 8
DTConstrIndDef{ F₁() -> non empty DTConstrStr , F₂() -> non empty set , F₃( set ) -> Element of F₂(), F₄( set , set , set ) -> Element of F₂() } :

ex f being Function of (TS F₁()),F₂() st
( ( for t being Symbol of F₁() st t in Terminals F₁() holds
f . (root-tree t) = F₃(t) ) & ( for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts holds
f . (nt -tree ts) = F₄(nt,(roots ts),(f * ts)) ) )

proof end;

scheme :: DTCONSTR:sch 9
DTConstrUniqDef{ F₁() -> non empty DTConstrStr , F₂() -> non empty set , F₃( set ) -> Element of F₂(), F₄( set , set , set ) -> Element of F₂(), F₅() -> Function of (TS F₁()),F₂(), F₆() -> Function of (TS F₁()),F₂() } :

F₅() = F₆()

provided

A1: ( ( for t being Symbol of F₁() st t in Terminals F₁() holds
F₅() . (root-tree t) = F₃(t) ) & ( for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts holds
F₅() . (nt -tree ts) = F₄(nt,(roots ts),(F₅() * ts)) ) ) and
A2: ( ( for t being Symbol of F₁() st t in Terminals F₁() holds
F₆() . (root-tree t) = F₃(t) ) & ( for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts holds
F₆() . (nt -tree ts) = F₄(nt,(roots ts),(F₆() * ts)) ) )

proof end;

definition

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

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines PeanoNat DTCONSTR:def 2 :

Lm8: now :: thesis:

given x being FinSequence such that A1: O ==> x ; :: thesis:
[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:

end;

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 :

:: deftheorem Def4 defines with_nonterminals DTCONSTR:def 4 :

:: deftheorem Def5 defines with_useful_nonterminals DTCONSTR:def 5 :

definition

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

proof end;

end;

registration

let G be non empty with_terminals DTConstrStr ;

cluster TS G -> non empty ;

coherence

proof end;

end;

registration

let G be non empty with_useful_nonterminals DTConstrStr ;

cluster TS G -> non empty ;

coherence

proof end;

end;

definition

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

proof end;

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

end;

:: deftheorem Def6 defines SubtreeSeq DTCONSTR:def 6 :

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

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;

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

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 ;

end;

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

definition

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

existence

proof end;

uniqueness

proof end;

end;

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

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 :

definition

func NAT-to-PN -> sequence of (TS PeanoNat) means :Def10: :: DTCONSTR:def 10
( it . 0 = root-tree 0 & ( for n being Nat holds it . (n + 1) = PNsucc (it . n) ) );

existence

proof end;

uniqueness

proof end;

end;

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

theorem :: DTCONSTR:11

for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)

proof end;

Lm18: now :: thesis:

let n be Element of NAT ; :: thesis:
assume A1: n = PN-to-NAT . (NAT-to-PN . n) ; :: thesis:
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:

end;

theorem :: DTCONSTR:12

for n being Nat holds n = PN-to-NAT . (NAT-to-PN . n)

proof end;

definition

let G be non empty DTConstrStr ;
let tsg be DecoratedTree of the carrier of G;
assume A1: tsg in TS G ;
defpred S₂[ object ] means $1 in Terminals G;
deffunc H₅( object ) -> set = <*$1*>;
deffunc H₆( object ) -> set = {} ;

A2: now :: thesis:

let x be object ; :: thesis:
assume x in the carrier of G ; :: thesis:

hereby :: thesis:

assume A3: S₂[x] ; :: thesis:
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₅(x) in (Terminals G) * ; :: thesis:

end;

assume not S₂[x] ; :: thesis:
<*> (Terminals G) = {} ;
hence H₆(x) in (Terminals G) * ; :: thesis:

end;

consider s2t being Function of the carrier of G,((Terminals G) *) such that
A4: for s being object st s in the carrier of G holds
( ( S₂[s] implies s2t . s = H₅(s) ) & ( not S₂[s] implies s2t . s = H₆(s) ) ) from FUNCT_2:sch 5(A2);
deffunc H₇( Symbol of G) -> Element of (Terminals G) * = s2t . $1;
deffunc H₈( set , set , FinSequence of (Terminals G) * ) -> Element of (Terminals G) * = FlattenSeq $3;
deffunc H₉( object ) -> set = <*$1*>;

func TerminalString tsg -> FinSequence of Terminals G means :Def11: :: DTCONSTR:def 11
ex f being Function of (TS G),((Terminals G) *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) );

existence

proof end;

uniqueness

proof end;

A17: now :: thesis:

let x be object ; :: thesis:
assume x in the carrier of G ; :: thesis:
then reconsider x9 = x as Element of G ;
<*x9*> is FinSequence of the carrier of G ;
hence H₉(x) in the carrier of G * ; :: thesis:

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 = H₉(s) from FUNCT_2:sch 2(A17);
deffunc H₁₀( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H₁₁( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3);

func PreTraversal tsg -> FinSequence of the carrier of G means :Def12: :: DTCONSTR:def 12
ex f being Function of (TS G),( the carrier of G *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) );

existence

proof end;

uniqueness

proof end;

deffunc H₁₂( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H₁₃( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (FlattenSeq $3) ^ (s2s . $1);

func PostTraversal tsg -> FinSequence of the carrier of G means :Def13: :: DTCONSTR:def 13
ex f being Function of (TS G),( the carrier of G *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines TerminalString DTCONSTR:def 11 :

:: deftheorem Def12 defines PreTraversal DTCONSTR:def 12 :

:: deftheorem Def13 defines PostTraversal DTCONSTR:def 13 :

definition

let G be non empty with_nonterminals DTConstrStr ;
let nt be Symbol of G;

func TerminalLanguage nt -> Subset of ((Terminals G) *) equals :: DTCONSTR:def 14
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;

coherence

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

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

proof end;

end;

:: deftheorem defines TerminalLanguage DTCONSTR:def 14 :

:: deftheorem defines PreTraversalLanguage DTCONSTR:def 15 :

:: deftheorem defines PostTraversalLanguage DTCONSTR:def 16 :

theorem Th13: :: DTCONSTR:13

for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
TerminalString t = <*0*>

proof end;

theorem :: DTCONSTR:14

for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}

proof end;

theorem Th15: :: DTCONSTR:15

for t being Element of TS PeanoNat holds PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>

proof end;

theorem :: DTCONSTR:16

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

proof end;

theorem Th17: :: DTCONSTR:17

for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)

proof end;

theorem :: DTCONSTR:18

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

proof end;