:: DTCONSTR semantic presentation
begin
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( set , set , set ) -> Element of NAT = 0 ;
theorem Th1: :: DTCONSTR:1
for D being non empty set
for p being FinSequence of FinTrees D holds p is FinSequence of Trees D
proof
let D be non empty set ; ::_thesis: for p being FinSequence of FinTrees D holds p is FinSequence of Trees D
FinTrees D is non empty Subset of (Trees D) by TREES_3:21;
hence for p being FinSequence of FinTrees D holds p is FinSequence of Trees D by FINSEQ_2:24; ::_thesis: verum
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
let x, y be set ; ::_thesis: for p being FinSequence of x st y in dom p holds
p . y in x
let p be FinSequence of x; ::_thesis: ( y in dom p implies p . y in x )
assume y in dom p ; ::_thesis: p . y in x
then A1: p . y in rng p by FUNCT_1:def_3;
rng p c= x by FINSEQ_1:def_4;
hence p . y in x by A1; ::_thesis: verum
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
let x be Element of Tset; ::_thesis: x is Element of F
thus x is Element of F ; ::_thesis: verum
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
let x be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not x in rng (roots p) or x in D )
assume x in rng (roots p) ; ::_thesis: x in D
then consider k being set such that
A1: k in dom (roots p) and
A2: x = (roots p) . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A1;
A3: dom (roots p) = dom p by TREES_3:def_18;
then consider t being DecoratedTree such that
A4: t = p . k and
A5: (roots p) . k = t . {} by A1, TREES_3:def_18;
reconsider t = t as DecoratedTree of D by A1, A3, A4, Th2, TREES_3:def_6;
reconsider r = {} as Node of t by TREES_1:22;
t . r in D ;
hence x in D by A2, A5; ::_thesis: verum
end;
end;
Lm1: dom (roots {}) = dom {} by TREES_3:def_18
.= {} ;
theorem Th3: :: DTCONSTR:3
roots {} = {} by Lm1;
theorem Th4: :: DTCONSTR:4
for T being DecoratedTree holds roots <*T*> = <*(T . {})*>
proof
let T be DecoratedTree; ::_thesis: roots <*T*> = <*(T . {})*>
A1: dom <*T*> = Seg 1 by FINSEQ_1:def_8;
A2: dom <*(T . {})*> = Seg 1 by FINSEQ_1:def_8;
A3: <*T*> . 1 = T by FINSEQ_1:def_8;
A4: <*(T . {})*> . 1 = T . {} by FINSEQ_1:def_8;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_<*T*>_holds_
ex_t_being_DecoratedTree_st_
(_t_=_<*T*>_._i_&_<*(T_._{})*>_._i_=_t_._{}_)
let i be Element of NAT ; ::_thesis: ( i in dom <*T*> implies ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {})*> . i = t . {} ) )
assume A5: i in dom <*T*> ; ::_thesis: ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {})*> . i = t . {} )
take t = T; ::_thesis: ( t = <*T*> . i & <*(T . {})*> . i = t . {} )
thus ( t = <*T*> . i & <*(T . {})*> . i = t . {} ) by A1, A3, A4, A5, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
hence roots <*T*> = <*(T . {})*> by A1, A2, TREES_3:def_18; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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 )
let F be Subset of (FinTrees D); ::_thesis: 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 )
let p be FinSequence of F; ::_thesis: ( len (roots p) = 1 implies ex x being Element of FinTrees D st
( p = <*x*> & x in F ) )
assume len (roots p) = 1 ; ::_thesis: ex x being Element of FinTrees D st
( p = <*x*> & x in F )
then A1: dom (roots p) = Seg 1 by FINSEQ_1:def_3;
A2: dom p = dom (roots p) by TREES_3:def_18;
then A3: 1 in dom p by A1;
then reconsider x = p . 1 as Element of FinTrees D by Th2;
take x ; ::_thesis: ( p = <*x*> & x in F )
thus ( p = <*x*> & x in F ) by A1, A2, A3, Th2, FINSEQ_1:def_8; ::_thesis: verum
end;
theorem :: DTCONSTR:6
for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>
proof
let T1, T2 be DecoratedTree; ::_thesis: roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: len <*(T1 . {}),(T2 . {})*> = 2 by FINSEQ_1:44;
A3: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A4: <*(T1 . {}),(T2 . {})*> . 1 = T1 . {} by FINSEQ_1:44;
A5: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
A6: <*(T1 . {}),(T2 . {})*> . 2 = T2 . {} by FINSEQ_1:44;
A7: dom <*T1,T2*> = Seg 2 by A1, FINSEQ_1:def_3;
A8: dom <*(T1 . {}),(T2 . {})*> = Seg 2 by A2, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_<*T1,T2*>_holds_
ex_t_being_DecoratedTree_st_
(_t_=_<*T1,T2*>_._i_&_<*(T1_._{}),(T2_._{})*>_._i_=_t_._{}_)
let i be Element of NAT ; ::_thesis: ( i in dom <*T1,T2*> implies ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) )
assume i in dom <*T1,T2*> ; ::_thesis: ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} )
then i in Seg 2 by A1, FINSEQ_1:def_3;
then ( i = 1 or i = 2 ) by FINSEQ_1:2, TARSKI:def_2;
hence ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) by A3, A4, A5, A6; ::_thesis: verum
end;
hence roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*> by A7, A8, TREES_3:def_18; ::_thesis: verum
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
A1: dom (pr1 f) = dom f by MCART_1:def_12;
dom f = Seg (len f) by FINSEQ_1:def_3;
then reconsider p = pr1 f as FinSequence by A1, FINSEQ_1:def_2;
rng p c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in X )
assume x in rng p ; ::_thesis: x in X
then consider i being set such that
A2: i in dom p and
A3: x = p . i by FUNCT_1:def_3;
A4: f . i in [:X,Y:] by A1, A2, Th2;
x = (f . i) `1 by A1, A2, A3, MCART_1:def_12;
hence x in X by A4, MCART_1:10; ::_thesis: verum
end;
hence pr1 f is FinSequence of X by FINSEQ_1:def_4; ::_thesis: verum
end;
:: original: pr2
redefine func pr2 f -> FinSequence of Y;
coherence
pr2 f is FinSequence of Y
proof
A5: dom (pr2 f) = dom f by MCART_1:def_13;
dom f = Seg (len f) by FINSEQ_1:def_3;
then reconsider p = pr2 f as FinSequence by A5, FINSEQ_1:def_2;
rng p c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Y )
assume x in rng p ; ::_thesis: x in Y
then consider i being set such that
A6: i in dom p and
A7: x = p . i by FUNCT_1:def_3;
A8: f . i in [:X,Y:] by A5, A6, Th2;
x = (f . i) `2 by A5, A6, A7, MCART_1:def_13;
hence x in Y by A8, MCART_1:10; ::_thesis: verum
end;
hence pr2 f is FinSequence of Y by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
theorem Th7: :: DTCONSTR:7
( pr1 {} = {} & pr2 {} = {} )
proof
set r = <*> [:{},{}:];
dom (pr1 (<*> [:{},{}:])) = dom {}
.= {} ;
hence pr1 {} = {} ; ::_thesis: pr2 {} = {}
dom (pr2 (<*> [:{},{}:])) = dom {}
.= {} ;
hence pr2 {} = {} ; ::_thesis: verum
end;
begin
registration
let A be non empty set ;
let R be Relation of A,(A *);
cluster DTConstrStr(# A,R #) -> non empty ;
coherence
not DTConstrStr(# A,R #) is empty ;
end;
scheme :: DTCONSTR:sch 1
DTConstrStrEx{ F1() -> non empty set , P1[ set , set ] } :
ex G being non empty strict DTConstrStr st
( the carrier of G = F1() & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P1[x,p] ) ) )
proof
consider PR being Relation of F1(),(F1() *) such that
A1: for x, y being set holds
( [x,y] in PR iff ( x in F1() & y in F1() * & P1[x,y] ) ) from RELSET_1:sch_1();
take DT = DTConstrStr(# F1(),PR #); ::_thesis: ( the carrier of DT = F1() & ( for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] ) ) )
thus the carrier of DT = F1() ; ::_thesis: for x being Symbol of DT
for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] )
let x be Symbol of DT; ::_thesis: for p being FinSequence of the carrier of DT holds
( x ==> p iff P1[x,p] )
let p be FinSequence of the carrier of DT; ::_thesis: ( x ==> p iff P1[x,p] )
hereby ::_thesis: ( P1[x,p] implies x ==> p )
assume x ==> p ; ::_thesis: P1[x,p]
then [x,p] in the Rules of DT by LANG1:def_1;
hence P1[x,p] by A1; ::_thesis: verum
end;
assume A2: P1[x,p] ; ::_thesis: x ==> p
p in the carrier of DT * by FINSEQ_1:def_11;
then [x,p] in PR by A1, A2;
hence x ==> p by LANG1:def_1; ::_thesis: verum
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
let G1, G2 be non empty strict DTConstrStr ; ::_thesis: ( 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] ) ) implies G1 = G2 )
assume that
A1: the carrier of G1 = F1() and
A2: for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff P1[x,p] ) and
A3: the carrier of G2 = F1() and
A4: for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff P1[x,p] ) ; ::_thesis: G1 = G2
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_the_Rules_of_G1_implies_[x,y]_in_the_Rules_of_G2_)_&_(_[x,y]_in_the_Rules_of_G2_implies_[x,y]_in_the_Rules_of_G1_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in the Rules of G1 implies [x,y] in the Rules of G2 ) & ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 ) )
hereby ::_thesis: ( [x,y] in the Rules of G2 implies [x,y] in the Rules of G1 )
assume A5: [x,y] in the Rules of G1 ; ::_thesis: [x,y] in the Rules of G2
then A6: y in the carrier of G1 * by ZFMISC_1:87;
reconsider x1 = x as Symbol of G1 by A5, ZFMISC_1:87;
reconsider y1 = y as FinSequence of the carrier of G1 by A6, FINSEQ_2:def_3;
A7: ( x1 ==> y1 iff P1[x1,y1] ) by A2;
reconsider x2 = x as Symbol of G2 by A1, A3, A5, ZFMISC_1:87;
reconsider y2 = y as FinSequence of the carrier of G2 by A1, A3, A6, FINSEQ_2:def_3;
x2 ==> y2 by A4, A5, A7, LANG1:def_1;
hence [x,y] in the Rules of G2 by LANG1:def_1; ::_thesis: verum
end;
assume A8: [x,y] in the Rules of G2 ; ::_thesis: [x,y] in the Rules of G1
then A9: y in the carrier of G2 * by ZFMISC_1:87;
reconsider x2 = x as Symbol of G2 by A8, ZFMISC_1:87;
reconsider y2 = y as FinSequence of the carrier of G2 by A9, FINSEQ_2:def_3;
A10: ( x2 ==> y2 iff P1[x2,y2] ) by A4;
reconsider x1 = x as Symbol of G1 by A1, A3, A8, ZFMISC_1:87;
reconsider y1 = y as FinSequence of the carrier of G1 by A1, A3, A9, FINSEQ_2:def_3;
x1 ==> y1 by A2, A8, A10, LANG1:def_1;
hence [x,y] in the Rules of G1 by LANG1:def_1; ::_thesis: verum
end;
hence G1 = G2 by A1, A3, RELAT_1:def_2; ::_thesis: verum
end;
theorem :: DTCONSTR:8
for G being non empty DTConstrStr holds Terminals G misses NonTerminals G
proof
let G be non empty DTConstrStr ; ::_thesis: Terminals G misses NonTerminals G
A1: Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def_2;
A2: NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def_3;
assume not Terminals G misses NonTerminals G ; ::_thesis: contradiction
then consider x being set such that
A3: x in Terminals G and
A4: x in NonTerminals G by XBOOLE_0:3;
A5: ex t being Symbol of G st
( x = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A1, A3;
ex t being Symbol of G st
( x = t & ex tnt being FinSequence st t ==> tnt ) by A2, A4;
hence contradiction by A5; ::_thesis: verum
end;
scheme :: DTCONSTR:sch 3
DTCMin{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex X being Subset of (FinTrees [: the carrier of F2(),F3():]) st
( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof
set f = F1();
set G = F2();
set D = F3();
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
Union F1() c= FinTrees [: the carrier of F2(),F3():]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Union F1() or u in FinTrees [: the carrier of F2(),F3():] )
assume u in Union F1() ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():]
then A4: ex k being set st
( k in NAT & u in F1() . k ) by A1, CARD_5:2;
defpred S1[ Element of NAT ] means for u being set st u in F1() . $1 holds
u in FinTrees [: the carrier of F2(),F3():];
A5: S1[ 0 ]
proof
let u be set ; ::_thesis: ( u in F1() . 0 implies u in FinTrees [: the carrier of F2(),F3():] )
assume u in F1() . 0 ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():]
then ex t being Symbol of F2() ex d being Element of F3() st
( u = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2;
hence u in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: verum
end;
A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let u be set ; ::_thesis: ( u in F1() . (n + 1) implies u in FinTrees [: the carrier of F2(),F3():] )
assume u in F1() . (n + 1) ; ::_thesis: u in FinTrees [: the carrier of F2(),F3():]
then u in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
then A8: ( u in F1() . n or u in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3;
assume A9: not u in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: contradiction
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A10: u = [o,H3(o,p)] -tree p and
A11: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A7, A8;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A11;
u = [o,H3(o,p)] -tree p by A10;
hence contradiction by A9; ::_thesis: verum
end;
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A6);
hence u in FinTrees [: the carrier of F2(),F3():] by A4; ::_thesis: verum
end;
then reconsider X = Union F1() as Subset of (FinTrees [: the carrier of F2(),F3():]) ;
take X ; ::_thesis: ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
thus X = Union F1() ; ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
hereby ::_thesis: ( ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
let d be Symbol of F2(); ::_thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in X )
assume d in Terminals F2() ; ::_thesis: root-tree [d,F4(d)] in X
then root-tree [d,F4(d)] in F1() . 0 by A2;
hence root-tree [d,F4(d)] in X by A1, CARD_5:2; ::_thesis: verum
end;
hereby ::_thesis: for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F
let o be Symbol of F2(); ::_thesis: for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X
let p be FinSequence of X; ::_thesis: ( o ==> pr1 (roots p) implies [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X )
assume A12: o ==> pr1 (roots p) ; ::_thesis: [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X
set s = pr1 (roots p);
set v = pr2 (roots p);
A13: dom p = Seg (len p) by FINSEQ_1:def_3;
defpred S1[ set , set ] means p . $1 in F1() . $2;
A14: for x being Nat st x in Seg (len p) holds
ex n being Element of NAT st S1[x,n]
proof
let x be Nat; ::_thesis: ( x in Seg (len p) implies ex n being Element of NAT st S1[x,n] )
assume x in Seg (len p) ; ::_thesis: ex n being Element of NAT st S1[x,n]
then A15: p . x in rng p by A13, FUNCT_1:def_3;
rng p c= X by FINSEQ_1:def_4;
then ex n being set st
( n in NAT & p . x in F1() . n ) by A1, A15, CARD_5:2;
hence ex n being Element of NAT st S1[x,n] ; ::_thesis: verum
end;
consider pn being FinSequence of NAT such that
A16: ( dom pn = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S1[k,pn . k] ) ) from FINSEQ_1:sch_5(A14);
A17: now__::_thesis:_(_rng_pn_<>_{}_implies_ex_n_being_Element_of_NAT_st_rng_p_c=_F1()_._n_)
defpred S2[ Element of NAT , Element of NAT ] means $1 >= $2;
assume rng pn <> {} ; ::_thesis: ex n being Element of NAT st rng p c= F1() . n
then A18: ( rng pn is finite & rng pn <> {} & rng pn c= NAT ) by FINSEQ_1:def_4;
A19: for x, y being Element of NAT holds
( S2[x,y] or S2[y,x] ) ;
A20: for x, y, z being Element of NAT st S2[x,y] & S2[y,z] holds
S2[x,z] by XXREAL_0:2;
consider n being Element of NAT such that
A21: ( n in rng pn & ( for y being Element of NAT st y in rng pn holds
S2[n,y] ) ) from CQC_SIM1:sch_4(A18, A19, A20);
take n = n; ::_thesis: rng p c= F1() . n
thus rng p c= F1() . n ::_thesis: verum
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng p or t in F1() . n )
assume t in rng p ; ::_thesis: t in F1() . n
then consider k being set such that
A22: k in dom p and
A23: t = p . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A22;
A24: pn . k in rng pn by A13, A16, A22, FUNCT_1:def_3;
then reconsider pnk = pn . k as Element of NAT by A18;
consider s being Nat such that
A25: n = pnk + s by A21, A24, NAT_1:10;
deffunc H4( set , set ) -> set = { ([o1,F5(o1,(pr1 (roots p1)),(pr2 (roots p1)))] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) } ;
for n being Element of NAT holds F1() . n c= F1() . (n + 1)
proof
let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1)
F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3;
hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum
end;
then A26: F1() . pnk c= F1() . n by A25, MEASURE2:18, NAT_1:11;
t in F1() . (pn . k) by A13, A16, A22, A23;
hence t in F1() . n by A26; ::_thesis: verum
end;
end;
now__::_thesis:_(_rng_pn_=_{}_implies_rng_p_c=_F1()_._0_)
assume rng pn = {} ; ::_thesis: rng p c= F1() . 0
then pn = {} ;
then p = {} by A16;
then rng p = {} ;
hence rng p c= F1() . 0 by XBOOLE_1:2; ::_thesis: verum
end;
then consider n being Element of NAT such that
A27: rng p c= F1() . n by A17;
A28: X = union (rng F1()) by CARD_3:def_4;
F1() . n in rng F1() by A1, FUNCT_1:def_3;
then F1() . n c= X by A28, ZFMISC_1:74;
then reconsider fn = F1() . n as Subset of (FinTrees [: the carrier of F2(),F3():]) by XBOOLE_1:1;
reconsider q = p as FinSequence of fn by A27, FINSEQ_1:def_4;
reconsider q9 = q as Element of fn * by FINSEQ_1:def_11;
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A12;
then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by XBOOLE_0:def_3;
then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in F1() . (n + 1) by A3;
hence [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X by A1, CARD_5:2; ::_thesis: verum
end;
let F be Subset of (FinTrees [: the carrier of F2(),F3():]); ::_thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) implies X c= F )
assume that
A29: for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F and
A30: for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in F ; ::_thesis: X c= F
defpred S1[ Element of NAT ] means F1() . $1 c= F;
A31: S1[ 0 ]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() . 0 or x in F )
reconsider p = <*> F as FinSequence of F ;
assume x in F1() . 0 ; ::_thesis: x in F
then consider t being Symbol of F2(), d being Element of F3() such that
A32: x = root-tree [t,d] and
A33: ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> pr1 (roots p) & d = H3(t,p) ) ) by A2, Th3, Th7;
[t,d] -tree p = root-tree [t,d] by TREES_4:20;
hence x in F by A29, A30, A32, A33; ::_thesis: verum
end;
A34: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A35: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() . (n + 1) or x in F )
assume that
A36: x in F1() . (n + 1) and
A37: not x in F ; ::_thesis: contradiction
x in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A3, A36;
then ( x in F1() . n or x in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3;
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A38: x = [o,H3(o,p)] -tree p and
A39: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A35, A37;
rng p c= F1() . n by FINSEQ_1:def_4;
then rng p c= F by A35, XBOOLE_1:1;
then reconsider p = p as FinSequence of F by FINSEQ_1:def_4;
o ==> pr1 (roots p) by A39;
hence contradiction by A30, A37, A38; ::_thesis: verum
end;
end;
A40: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A31, A34);
thus X c= F ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in F )
assume x in X ; ::_thesis: x in F
then consider n being set such that
A41: n in NAT and
A42: x in F1() . n by A1, CARD_5:2;
F1() . n c= F by A40, A41;
hence x in F by A42; ::_thesis: verum
end;
end;
scheme :: DTCONSTR:sch 4
DTCSymbols{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
ex X1 being Subset of (FinTrees the carrier of F2()) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in X1 ) & ( for o being Symbol of F2()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F2()) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof
set f = F1();
set G = F2();
set D = F3();
set S = the carrier of F2();
set SxD = [: the carrier of F2(),F3():];
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
A4: 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,{},{}) ) ) } by A2;
A5: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
consider X being Subset of (FinTrees [: the carrier of F2(),F3():]) such that
A6: ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) ) from DTCONSTR:sch_3(A1, A4, A5);
set X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ;
{ (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } c= FinTrees the carrier of F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } or x in FinTrees the carrier of F2() )
assume x in { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ; ::_thesis: x in FinTrees the carrier of F2()
then consider tt being Element of FinTrees [: the carrier of F2(),F3():] such that
A7: x = tt `1 and
tt in Union F1() ;
A8: tt `1 = (pr1 ( the carrier of F2(),F3())) * tt by TREES_3:def_12;
A9: rng tt c= [: the carrier of F2(),F3():] by RELAT_1:def_19;
dom (pr1 ( the carrier of F2(),F3())) = [: the carrier of F2(),F3():] by FUNCT_2:def_1;
then dom (tt `1) = dom tt by A8, A9, RELAT_1:27;
hence x in FinTrees the carrier of F2() by A7, TREES_3:def_8; ::_thesis: verum
end;
then reconsider X9 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } as Subset of (FinTrees the carrier of F2()) ;
take X1 = X9; ::_thesis: ( 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 ) )
thus X1 = { (t `1) where t is Element of FinTrees [: the carrier of F2(),F3():] : t in Union F1() } ; ::_thesis: ( ( 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 ) )
hereby ::_thesis: ( ( 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 ) )
let t be Symbol of F2(); ::_thesis: ( t in Terminals F2() implies root-tree t in X1 )
assume A10: t in Terminals F2() ; ::_thesis: root-tree t in X1
A11: (root-tree [t,F4(t)]) `1 = root-tree t by TREES_4:25;
root-tree [t,F4(t)] in Union F1() by A6, A10;
hence root-tree t in X1 by A11; ::_thesis: verum
end;
hereby ::_thesis: 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
let nt be Symbol of F2(); ::_thesis: for ts being FinSequence of X1 st nt ==> roots ts holds
nt -tree ts in X1
let ts be FinSequence of X1; ::_thesis: ( nt ==> roots ts implies nt -tree ts in X1 )
assume A12: nt ==> roots ts ; ::_thesis: nt -tree ts in X1
A13: dom ts = Seg (len ts) by FINSEQ_1:def_3;
defpred S1[ set , set ] means ex dt being DecoratedTree of [: the carrier of F2(),F3():] st
( dt = $2 & dt `1 = ts . $1 & dt in Union F1() );
A14: for k being Nat st k in Seg (len ts) holds
ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] )
assume k in Seg (len ts) ; ::_thesis: ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x]
then A15: ts . k in rng ts by A13, FUNCT_1:def_3;
rng ts c= X1 by FINSEQ_1:def_4;
then ts . k in X1 by A15;
then ex x being Element of FinTrees [: the carrier of F2(),F3():] st
( ts . k = x `1 & x in Union F1() ) ;
hence ex x being Element of FinTrees [: the carrier of F2(),F3():] st S1[k,x] ; ::_thesis: verum
end;
consider dts being FinSequence of FinTrees [: the carrier of F2(),F3():] such that
A16: dom dts = Seg (len ts) and
A17: for k being Nat st k in Seg (len ts) holds
S1[k,dts . k] from FINSEQ_1:sch_5(A14);
rng dts c= Union F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng dts or x in Union F1() )
assume x in rng dts ; ::_thesis: x in Union F1()
then consider k being set such that
A18: k in dom ts and
A19: x = dts . k by A13, A16, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A18;
ex dt being DecoratedTree of [: the carrier of F2(),F3():] st
( dt = x & dt `1 = ts . k & dt in Union F1() ) by A13, A17, A18, A19;
hence x in Union F1() ; ::_thesis: verum
end;
then reconsider dts = dts as FinSequence of X by A6, FINSEQ_1:def_4;
A20: dom (roots ts) = dom ts by TREES_3:def_18;
A21: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def_12;
then A22: dom (pr1 (roots dts)) = dom ts by A13, A16, TREES_3:def_18;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_
(roots_ts)_._k_=_(pr1_(roots_dts))_._k
let k be Nat; ::_thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A23: k in dom ts ; ::_thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F2(),F3():] such that
A24: dt = dts . k and
A25: dt `1 = ts . k and
dt in Union F1() by A13, A17;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A23, TREES_3:def_18;
then A26: (roots ts) . k = (dt . r) `1 by A25, TREES_3:39;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A13, A16, A23, TREES_3:def_18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A21, A22, A23, A24, A26, MCART_1:def_12; ::_thesis: verum
end;
then roots ts = pr1 (roots dts) by A20, A22, FINSEQ_1:13;
then A27: [nt,H3(nt,dts)] -tree dts in X by A6, A12;
A28: rng dts c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4;
FinTrees [: the carrier of F2(),F3():] c= Trees [: the carrier of F2(),F3():] by TREES_3:21;
then rng dts c= Trees [: the carrier of F2(),F3():] by A28, XBOOLE_1:1;
then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F2(),F3():] by FINSEQ_1:def_4;
A29: rng ts c= FinTrees the carrier of F2() by FINSEQ_1:def_4;
FinTrees the carrier of F2() c= Trees the carrier of F2() by TREES_3:21;
then rng ts c= Trees the carrier of F2() by A29, XBOOLE_1:1;
then reconsider ts9 = ts as FinSequence of Trees the carrier of F2() by FINSEQ_1:def_4;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_dts_holds_
for_T_being_DecoratedTree_of_[:_the_carrier_of_F2(),F3():]_st_T_=_dts_._i_holds_
ts_._i_=_T_`1
let i be Element of NAT ; ::_thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; ::_thesis: for T being DecoratedTree of [: the carrier of F2(),F3():] st T = dts . i holds
ts . i = T `1
then A30: ex dt being DecoratedTree of [: the carrier of F2(),F3():] st
( dt = dts . i & dt `1 = ts . i & dt in Union F1() ) by A16, A17;
let T be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; ::_thesis: ts . i = T `1
hence ts . i = T `1 by A30; ::_thesis: verum
end;
then ([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A13, A16, TREES_4:27;
hence nt -tree ts in X1 by A6, A27; ::_thesis: verum
end;
let F be Subset of (FinTrees the carrier of F2()); ::_thesis: ( ( 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 ) implies X1 c= F )
assume that
A31: for d being Symbol of F2() st d in Terminals F2() holds
root-tree d in F and
A32: for o being Symbol of F2()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ; ::_thesis: X1 c= F
thus X1 c= F ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in F )
assume x in X1 ; ::_thesis: x in F
then consider tt being Element of FinTrees [: the carrier of F2(),F3():] such that
A33: x = tt `1 and
A34: tt in Union F1() ;
set FF = { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ;
{ dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } c= FinTrees [: the carrier of F2(),F3():]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } or x in FinTrees [: the carrier of F2(),F3():] )
assume x in { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } ; ::_thesis: x in FinTrees [: the carrier of F2(),F3():]
then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( x = dt & dt `1 in F ) ;
hence x in FinTrees [: the carrier of F2(),F3():] ; ::_thesis: verum
end;
then reconsider FF = { dt where dt is Element of FinTrees [: the carrier of F2(),F3():] : dt `1 in F } as Subset of (FinTrees [: the carrier of F2(),F3():]) ;
A35: now__::_thesis:_for_d_being_Symbol_of_F2()_st_d_in_Terminals_F2()_holds_
root-tree_[d,F4(d)]_in_FF
let d be Symbol of F2(); ::_thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in FF )
assume d in Terminals F2() ; ::_thesis: root-tree [d,F4(d)] in FF
then A36: root-tree d in F by A31;
(root-tree [d,F4(d)]) `1 = root-tree d by TREES_4:25;
hence root-tree [d,F4(d)] in FF by A36; ::_thesis: verum
end;
now__::_thesis:_for_o_being_Symbol_of_F2()
for_p_being_FinSequence_of_FF_st_o_==>_pr1_(roots_p)_holds_
[o,H3(o,p)]_-tree_p_in_FF
let o be Symbol of F2(); ::_thesis: for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in FF
let p be FinSequence of FF; ::_thesis: ( o ==> pr1 (roots p) implies [o,H3(o,p)] -tree p in FF )
assume A37: o ==> pr1 (roots p) ; ::_thesis: [o,H3(o,p)] -tree p in FF
consider p1 being FinSequence of FinTrees the carrier of F2() such that
A38: dom p1 = dom p and
A39: for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [: the carrier of F2(),F3():] st
( T = p . i & p1 . i = T `1 ) and
A40: ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 = o -tree p1 by TREES_4:31;
rng p1 c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p1 or x in F )
assume x in rng p1 ; ::_thesis: x in F
then consider k being set such that
A41: k in dom p1 and
A42: x = p1 . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A41;
A43: p . k in rng p by A38, A41, FUNCT_1:def_3;
A44: ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( dt = p . k & x = dt `1 ) by A38, A39, A41, A42;
rng p c= FF by FINSEQ_1:def_4;
then p . k in FF by A43;
then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( p . k = dt & dt `1 in F ) ;
hence x in F by A44; ::_thesis: verum
end;
then reconsider p1 = p1 as FinSequence of F by FINSEQ_1:def_4;
A45: dom (roots p1) = dom p1 by TREES_3:def_18;
A46: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def_12;
then A47: dom (pr1 (roots p)) = dom p1 by A38, TREES_3:def_18;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p1_holds_
(roots_p1)_._k_=_(pr1_(roots_p))_._k
let k be Nat; ::_thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )
assume A48: k in dom p1 ; ::_thesis: (roots p1) . k = (pr1 (roots p)) . k
then A49: p . k in rng p by A38, FUNCT_1:def_3;
A50: ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( dt = p . k & p1 . k = dt `1 ) by A38, A39, A48;
rng p c= FF by FINSEQ_1:def_4;
then p . k in FF by A49;
then consider dt being Element of FinTrees [: the carrier of F2(),F3():] such that
A51: p . k = dt and
dt `1 in F ;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = p1 . k & (roots p1) . k = T . {} ) by A48, TREES_3:def_18;
then A52: (roots p1) . k = (dt . r) `1 by A50, A51, TREES_3:39;
ex T being DecoratedTree st
( T = p . k & (roots p) . k = T . {} ) by A38, A48, TREES_3:def_18;
hence (roots p1) . k = (pr1 (roots p)) . k by A46, A47, A48, A51, A52, MCART_1:def_12; ::_thesis: verum
end;
then pr1 (roots p) = roots p1 by A45, A47, FINSEQ_1:13;
then ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 in F by A32, A37, A40;
hence [o,H3(o,p)] -tree p in FF ; ::_thesis: verum
end;
then X c= FF by A6, A35;
then tt in FF by A6, A34;
then ex dt being Element of FinTrees [: the carrier of F2(),F3():] st
( tt = dt & dt `1 in F ) ;
hence x in F by A33; ::_thesis: verum
end;
end;
scheme :: DTCONSTR:sch 5
DTCHeight{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for n being Element of NAT
for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . n iff height (dom dt) <= n )
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof
set f = F1();
set G = F2();
set D = F3();
set SxD = [: the carrier of F2(),F3():];
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
defpred S1[ Element of NAT ] means for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . $1 iff height (dom dt) <= $1 );
A4: S1[ 0 ]
proof
let dt be Element of FinTrees [: the carrier of F2(),F3():]; ::_thesis: ( dt in Union F1() implies ( dt in F1() . 0 iff height (dom dt) <= 0 ) )
assume A5: dt in Union F1() ; ::_thesis: ( dt in F1() . 0 iff height (dom dt) <= 0 )
hereby ::_thesis: ( height (dom dt) <= 0 implies dt in F1() . 0 )
assume dt in F1() . 0 ; ::_thesis: height (dom dt) <= 0
then ex t being Symbol of F2() ex d being Element of F3() st
( dt = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2;
hence height (dom dt) <= 0 by TREES_1:42, TREES_4:3; ::_thesis: verum
end;
assume height (dom dt) <= 0 ; ::_thesis: dt in F1() . 0
then A6: height (dom dt) = 0 ;
defpred S2[ Element of NAT ] means not dt in F1() . $1;
assume A7: S2[ 0 ] ; ::_thesis: contradiction
A8: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A9: S2[n] ; ::_thesis: S2[n + 1]
thus S2[n + 1] ::_thesis: verum
proof
assume dt in F1() . (n + 1) ; ::_thesis: contradiction
then dt in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
then ( dt in F1() . n or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3;
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A10: dt = [o,H3(o,p)] -tree p and
A11: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A9;
A12: dt = root-tree (dt . {}) by A6, TREES_1:43, TREES_4:5;
then A13: p = {} by A10, A11, TREES_4:17;
then dt = root-tree [o,F5(o,{},{})] by A10, A12, Th3, Th7, TREES_4:def_4;
hence contradiction by A2, A7, A11, A13, Th3, Th7; ::_thesis: verum
end;
end;
A14: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A7, A8);
ex n being set st
( n in NAT & dt in F1() . n ) by A1, A5, CARD_5:2;
hence contradiction by A14; ::_thesis: verum
end;
A15: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A16: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let dt be Element of FinTrees [: the carrier of F2(),F3():]; ::_thesis: ( dt in Union F1() implies ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 ) )
assume A17: dt in Union F1() ; ::_thesis: ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 )
hereby ::_thesis: ( height (dom dt) <= n + 1 implies dt in F1() . (n + 1) )
assume dt in F1() . (n + 1) ; ::_thesis: height (dom dt) <= n + 1
then dt in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
then A18: ( dt in F1() . n or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3;
percases ( dt in F1() . n or not dt in F1() . n ) ;
suppose dt in F1() . n ; ::_thesis: height (dom dt) <= n + 1
then A19: height (dom dt) <= n by A16, A17;
n <= n + 1 by NAT_1:11;
hence height (dom dt) <= n + 1 by A19, XXREAL_0:2; ::_thesis: verum
end;
suppose not dt in F1() . n ; ::_thesis: height (dom dt) <= n + 1
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A20: dt = [o,H3(o,p)] -tree p and
A21: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A18;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A21;
A22: dom dt = tree (doms p) by A20, TREES_4:10;
now__::_thesis:_for_t_being_finite_Tree_st_t_in_rng_(doms_p)_holds_
height_t_<=_n
let t be finite Tree; ::_thesis: ( t in rng (doms p) implies height t <= n )
assume t in rng (doms p) ; ::_thesis: height t <= n
then consider k being set such that
A23: k in dom (doms p) and
A24: t = (doms p) . k by FUNCT_1:def_3;
A25: k in dom p by A23, TREES_3:37;
then A26: p . k in rng p by FUNCT_1:def_3;
rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4;
then reconsider pk = p . k as Element of FinTrees [: the carrier of F2(),F3():] by A26;
A27: rng p c= F1() . n by FINSEQ_1:def_4;
A28: t = dom pk by A24, A25, FUNCT_6:22;
pk in Union F1() by A1, A26, A27, CARD_5:2;
hence height t <= n by A16, A26, A27, A28; ::_thesis: verum
end;
hence height (dom dt) <= n + 1 by A22, TREES_3:77; ::_thesis: verum
end;
end;
end;
assume A29: height (dom dt) <= n + 1 ; ::_thesis: dt in F1() . (n + 1)
defpred S2[ Nat] means dt in F1() . $1;
ex k being set st
( k in NAT & dt in F1() . k ) by A1, A17, CARD_5:2;
then A30: ex k being Nat st S2[k] ;
consider mk being Nat such that
A31: ( S2[mk] & ( for kk being Nat st S2[kk] holds
mk <= kk ) ) from NAT_1:sch_5(A30);
deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ;
A32: for n being Element of NAT holds F1() . n c= F1() . (n + 1)
proof
let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1)
F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3;
hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum
end;
percases ( mk = 0 or ex k being Nat st mk = k + 1 ) by NAT_1:6;
suppose mk = 0 ; ::_thesis: dt in F1() . (n + 1)
then F1() . mk c= F1() . (0 + (n + 1)) by A32, MEASURE2:18;
hence dt in F1() . (n + 1) by A31; ::_thesis: verum
end;
suppose ex k being Nat st mk = k + 1 ; ::_thesis: dt in F1() . (n + 1)
then consider k being Nat such that
A33: mk = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A34: k < k + 1 by NAT_1:13;
F1() . mk = (F1() . k) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3, A33;
then ( dt in F1() . k or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by A31, XBOOLE_0:def_3;
then consider o being Symbol of F2(), p being Element of (F1() . k) * such that
A35: dt = [o,H3(o,p)] -tree p and
A36: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A31, A33, A34;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A36;
A37: dom dt = tree (doms p) by A35, TREES_4:10;
rng p c= F1() . n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() . n )
assume x in rng p ; ::_thesis: x in F1() . n
then consider k9 being set such that
A38: k9 in dom p and
A39: x = p . k9 by FUNCT_1:def_3;
A40: x in rng p by A38, A39, FUNCT_1:def_3;
rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def_4;
then reconsider t = x as Element of FinTrees [: the carrier of F2(),F3():] by A40;
A41: k9 in dom (doms p) by A38, A39, FUNCT_6:22;
dom t = (doms p) . k9 by A38, A39, FUNCT_6:22;
then dom t in rng (doms p) by A41, FUNCT_1:def_3;
then height (dom t) < n + 1 by A29, A37, TREES_3:78, XXREAL_0:2;
then A42: height (dom t) <= n by NAT_1:13;
A43: rng p c= F1() . k by FINSEQ_1:def_4;
t in rng p by A38, A39, FUNCT_1:def_3;
then t in Union F1() by A1, A43, CARD_5:2;
hence x in F1() . n by A16, A42; ::_thesis: verum
end;
then p is FinSequence of F1() . n by FINSEQ_1:def_4;
then reconsider p = p as Element of (F1() . n) * by FINSEQ_1:def_11;
[o,H3(o,p)] -tree p in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A36;
then dt in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A35, XBOOLE_0:def_3;
hence dt in F1() . (n + 1) by A3; ::_thesis: verum
end;
end;
end;
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A15); ::_thesis: verum
end;
scheme :: DTCONSTR:sch 6
DTCUniq{ F1() -> Function, F2() -> non empty DTConstrStr , F3() -> non empty set , F4( set ) -> Element of F3(), F5( set , set , set ) -> Element of F3() } :
for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 holds
dt1 = dt2
provided
A1: dom F1() = NAT and
A2: F1() . 0 = { (root-tree [t,d]) where t is Symbol of F2(), d is Element of F3() : ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) } and
A3: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) }
proof
set f = F1();
set G = F2();
set D = F3();
set S = the carrier of F2();
set SxD = [: the carrier of F2(),F3():];
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
A4: 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,{},{}) ) ) } by A2;
A5: for n being Element of NAT holds F1() . (n + 1) = (F1() . n) \/ { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
defpred S1[ Element of NAT ] means for dt1, dt2 being DecoratedTree of [: the carrier of F2(),F3():] st dt1 in F1() . $1 & dt2 in F1() . $1 & dt1 `1 = dt2 `1 holds
dt1 = dt2;
A6: S1[ 0 ]
proof
let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in F1() . 0 & dt2 in F1() . 0 & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that
A7: dt1 in F1() . 0 and
A8: dt2 in F1() . 0 and
A9: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2
consider t1 being Symbol of F2(), d1 being Element of F3() such that
A10: dt1 = root-tree [t1,d1] and
A11: ( ( t1 in Terminals F2() & d1 = F4(t1) ) or ( t1 ==> {} & d1 = F5(t1,{},{}) ) ) by A2, A7;
consider t2 being Symbol of F2(), d2 being Element of F3() such that
A12: dt2 = root-tree [t2,d2] and
A13: ( ( t2 in Terminals F2() & d2 = F4(t2) ) or ( t2 ==> {} & d2 = F5(t2,{},{}) ) ) by A2, A8;
A14: root-tree t1 = dt1 `1 by A10, TREES_4:25;
root-tree t2 = dt2 `1 by A12, TREES_4:25;
then A15: t1 = t2 by A9, A14, TREES_4:4;
now__::_thesis:_for_t_being_Symbol_of_F2()_st_t_==>_{}_holds_
not_t_in_Terminals_F2()
let t be Symbol of F2(); ::_thesis: ( t ==> {} implies not t in Terminals F2() )
assume t ==> {} ; ::_thesis: not t in Terminals F2()
then for t9 being Symbol of F2() holds
( not t = t9 or ex tnt being FinSequence st t9 ==> tnt ) ;
then not t in { t9 where t9 is Symbol of F2() : for tnt being FinSequence holds not t9 ==> tnt } ;
hence not t in Terminals F2() by LANG1:def_2; ::_thesis: verum
end;
hence dt1 = dt2 by A10, A11, A12, A13, A15; ::_thesis: verum
end;
A16: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A17: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in F1() . (n + 1) & dt2 in F1() . (n + 1) & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that
A18: dt1 in F1() . (n + 1) and
A19: dt2 in F1() . (n + 1) and
A20: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2
A21: dom dt1 = dom (dt1 `1) by TREES_4:24;
A22: dom dt2 = dom (dt1 `1) by A20, TREES_4:24;
A23: dt1 in Union F1() by A1, A18, CARD_5:2;
A24: dt2 in Union F1() by A1, A19, CARD_5:2;
ex X being Subset of (FinTrees [: the carrier of F2(),F3():]) st
( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) ) from DTCONSTR:sch_3(A1, A4, A5);
then reconsider dt19 = dt1, dt29 = dt2 as Element of FinTrees [: the carrier of F2(),F3():] by A23, A24;
A25: for n being Element of NAT
for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . n iff height (dom dt) <= n ) from DTCONSTR:sch_5(A1, A4, A5);
percases ( dt1 in F1() . n or not dt1 in F1() . n ) ;
supposeA26: dt1 in F1() . n ; ::_thesis: dt1 = dt2
then height (dom dt19) <= n by A23, A25;
then dt29 in F1() . n by A21, A22, A24, A25;
hence dt1 = dt2 by A17, A20, A26; ::_thesis: verum
end;
supposeA27: not dt1 in F1() . n ; ::_thesis: dt1 = dt2
A28: F1() . (n + 1) = (F1() . n) \/ { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) } by A3;
then ( dt1 in F1() . n or dt1 in { ([o1,H3(o1,p1)] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) } ) by A18, XBOOLE_0:def_3;
then consider o1 being Symbol of F2(), p1 being Element of (F1() . n) * such that
A29: dt1 = [o1,H3(o1,p1)] -tree p1 and
A30: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) by A27;
height (dom dt19) > n by A23, A25, A27;
then A31: not dt29 in F1() . n by A21, A22, A24, A25;
( dt2 in F1() . n or dt2 in { ([o2,H3(o2,p2)] -tree p2) where o2 is Symbol of F2(), p2 is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p2 = q & o2 ==> pr1 (roots q) ) } ) by A19, A28, XBOOLE_0:def_3;
then consider o2 being Symbol of F2(), p2 being Element of (F1() . n) * such that
A32: dt2 = [o2,H3(o2,p2)] -tree p2 and
A33: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p2 = q & o2 ==> pr1 (roots q) ) by A31;
reconsider p1 = p1 as FinSequence of FinTrees [: the carrier of F2(),F3():] by A30;
consider p11 being FinSequence of FinTrees the carrier of F2() such that
A34: dom p11 = dom p1 and
A35: for i being Element of NAT st i in dom p1 holds
ex T being Element of FinTrees [: the carrier of F2(),F3():] st
( T = p1 . i & p11 . i = T `1 ) and
A36: ([o1,H3(o1,p1)] -tree p1) `1 = o1 -tree p11 by TREES_4:31;
reconsider p2 = p2 as FinSequence of FinTrees [: the carrier of F2(),F3():] by A33;
consider p21 being FinSequence of FinTrees the carrier of F2() such that
A37: dom p21 = dom p2 and
A38: for i being Element of NAT st i in dom p2 holds
ex T being Element of FinTrees [: the carrier of F2(),F3():] st
( T = p2 . i & p21 . i = T `1 ) and
A39: ([o2,H3(o2,p2)] -tree p2) `1 = o2 -tree p21 by TREES_4:31;
A40: o1 = o2 by A20, A29, A32, A36, A39, TREES_4:15;
A41: p11 = p21 by A20, A29, A32, A36, A39, TREES_4:15;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p11_holds_
p1_._k_=_p2_._k
let k be Nat; ::_thesis: ( k in dom p11 implies p1 . k = p2 . k )
assume A42: k in dom p11 ; ::_thesis: p1 . k = p2 . k
then consider p1k being Element of FinTrees [: the carrier of F2(),F3():] such that
A43: p1k = p1 . k and
A44: p11 . k = p1k `1 by A34, A35;
consider p2k being Element of FinTrees [: the carrier of F2(),F3():] such that
A45: p2k = p2 . k and
A46: p21 . k = p2k `1 by A37, A38, A41, A42;
A47: p1k in F1() . n by A34, A42, A43, Th2;
p2k in F1() . n by A37, A41, A42, A45, Th2;
hence p1 . k = p2 . k by A17, A41, A43, A44, A45, A46, A47; ::_thesis: verum
end;
then p1 = p2 by A34, A37, A41, FINSEQ_1:13;
hence dt1 = dt2 by A29, A32, A40; ::_thesis: verum
end;
end;
end;
end;
A48: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A16);
let dt1, dt2 be DecoratedTree of [: the carrier of F2(),F3():]; ::_thesis: ( dt1 in Union F1() & dt2 in Union F1() & dt1 `1 = dt2 `1 implies dt1 = dt2 )
assume that
A49: dt1 in Union F1() and
A50: dt2 in Union F1() and
A51: dt1 `1 = dt2 `1 ; ::_thesis: dt1 = dt2
consider n1 being set such that
A52: n1 in NAT and
A53: dt1 in F1() . n1 by A1, A49, CARD_5:2;
consider n2 being set such that
A54: n2 in NAT and
A55: dt2 in F1() . n2 by A1, A50, CARD_5:2;
reconsider n1 = n1, n2 = n2 as Element of NAT by A52, A54;
deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ;
A56: for n being Element of NAT holds F1() . n c= F1() . (n + 1)
proof
let n be Element of NAT ; ::_thesis: F1() . n c= F1() . (n + 1)
F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3;
hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; ::_thesis: verum
end;
A57: for k, s being Nat holds F1() . k c= F1() . (k + s)
proof
let k, s be Nat; ::_thesis: F1() . k c= F1() . (k + s)
reconsider k = k, s = s as Element of NAT by ORDINAL1:def_12;
k <= k + s by NAT_1:11;
hence F1() . k c= F1() . (k + s) by A56, MEASURE2:18; ::_thesis: verum
end;
( n1 <= n2 or n1 >= n2 ) ;
then ( ex s being Nat st n2 = n1 + s or ex s being Nat st n1 = n2 + s ) by NAT_1:10;
then ( F1() . n1 c= F1() . n2 or F1() . n2 c= F1() . n1 ) by A57;
hence dt1 = dt2 by A48, A51, A53, A55; ::_thesis: verum
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
deffunc H3( set , set ) -> set = $2 \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of G, p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of G,NAT:] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = { (root-tree [t,d]) where t is Symbol of G, d is Element of NAT : ( ( t in Terminals G & d = H1(t) ) or ( t ==> {} & d = H2(t, {} , {} ) ) ) } and
A3: for n being Nat holds f . (n + 1) = H3(n,f . n) from NAT_1:sch_11();
A4: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of G, p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of G,NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A3;
ex X1 being Subset of (FinTrees the carrier of G) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of G,NAT:] : t in Union f } & ( for d being Symbol of G st d in Terminals G holds
root-tree d in X1 ) & ( for o being Symbol of G
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 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
X1 c= F ) ) from DTCONSTR:sch_4(A1, A2, A4);
hence 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 ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in b1 ) & ( for o being Symbol of G
for p being FinSequence of b1 st o ==> roots p holds
o -tree p in b1 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) holds
b1 = b2
proof
let TSG1, TSG2 be Subset of (FinTrees the carrier of G); ::_thesis: ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG1 ) & ( for o being Symbol of G
for p being FinSequence of TSG1 st o ==> roots p holds
o -tree p in TSG1 ) & ( 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
TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG2 ) & ( for o being Symbol of G
for p being FinSequence of TSG2 st o ==> roots p holds
o -tree p in TSG2 ) & ( 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
TSG2 c= F ) implies TSG1 = TSG2 )
assume A5: ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG1 ) & ( for o being Symbol of G
for p being FinSequence of TSG1 st o ==> roots p holds
o -tree p in TSG1 ) & ( 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
TSG1 c= F ) & ( for d being Symbol of G st d in Terminals G holds
root-tree d in TSG2 ) & ( for o being Symbol of G
for p being FinSequence of TSG2 st o ==> roots p holds
o -tree p in TSG2 ) & ( 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
TSG2 c= F ) & not TSG1 = TSG2 ) ; ::_thesis: contradiction
then A6: TSG1 c= TSG2 ;
TSG2 c= TSG1 by A5;
hence contradiction by A5, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines TS DTCONSTR:def_1_:_
for G being non empty DTConstrStr
for b2 being Subset of (FinTrees the carrier of G) holds
( b2 = TS G iff ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b2 ) & ( for o being Symbol of G
for p being FinSequence of b2 st o ==> roots p holds
o -tree p in b2 ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b2 c= F ) ) );
scheme :: DTCONSTR:sch 7
DTConstrInd{ F1() -> non empty DTConstrStr , P1[ set ] } :
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
P1[t]
provided
A1: for s being Symbol of F1() st s in Terminals F1() holds
P1[ root-tree s] and
A2: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
deffunc H3( set , set ) -> set = $2 \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A3: dom f = NAT and
A4: f . 0 = { (root-tree [t,d]) where t is Symbol of F1(), d is Element of NAT : ( ( t in Terminals F1() & d = H1(t) ) or ( t ==> {} & d = H2(t, {} , {} ) ) ) } and
A5: for n being Nat holds f . (n + 1) = H3(n,f . n) from NAT_1:sch_11();
A6: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A5;
A7: ex X being Subset of (FinTrees [: the carrier of F1(),NAT:]) st
( X = Union f & ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,H1(d)] in X ) & ( for o being Symbol of F1()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F1(),NAT:]) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,H1(d)] in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in F ) holds
X c= F ) ) from DTCONSTR:sch_3(A3, A4, A6);
consider TSG being Subset of (FinTrees the carrier of F1()) such that
A8: TSG = { (t `1) where t is Element of FinTrees [: the carrier of F1(),NAT:] : t in Union f } and
A9: for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in TSG and
A10: for o being Symbol of F1()
for p being FinSequence of TSG st o ==> roots p holds
o -tree p in TSG and
A11: for F being Subset of (FinTrees the carrier of F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG c= F from DTCONSTR:sch_4(A3, A4, A6);
A12: TSG = TS F1() by A9, A10, A11, Def1;
defpred S1[ Element of NAT ] means for t being DecoratedTree of [: the carrier of F1(),NAT:] st t in f . $1 holds
P1[t `1 ];
A13: S1[ 0 ]
proof
let tt be DecoratedTree of [: the carrier of F1(),NAT:]; ::_thesis: ( tt in f . 0 implies P1[tt `1 ] )
set p = <*> (TS F1());
assume tt in f . 0 ; ::_thesis: P1[tt `1 ]
then consider t being Symbol of F1(), d being Element of NAT such that
A14: tt = root-tree [t,d] and
A15: ( ( t in Terminals F1() & d = 0 ) or ( t ==> roots (<*> (TS F1())) & d = 0 ) ) by A4, Th3;
A16: tt `1 = root-tree t by A14, TREES_4:25;
A17: t -tree (<*> (TS F1())) = root-tree t by TREES_4:20;
for T being DecoratedTree of the carrier of F1() st T in rng (<*> (TS F1())) holds
P1[T] ;
hence P1[tt `1 ] by A1, A2, A15, A16, A17; ::_thesis: verum
end;
A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A19: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let x be DecoratedTree of [: the carrier of F1(),NAT:]; ::_thesis: ( x in f . (n + 1) implies P1[x `1 ] )
assume that
A20: x in f . (n + 1) and
A21: P1[x `1 ] ; ::_thesis: contradiction
x in (f . n) \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A5, A20;
then ( x in f . n or x in { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def_3;
then consider o being Symbol of F1(), p being Element of (f . n) * such that
A22: x = [o,0] -tree p and
A23: ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) by A19, A21;
A24: Union f = union (rng f) by CARD_3:def_4;
A25: f . n in rng f by A3, FUNCT_1:def_3;
A26: rng p c= f . n by FINSEQ_1:def_4;
A27: f . n c= Union f by A24, A25, ZFMISC_1:74;
A28: dom p = Seg (len p) by FINSEQ_1:def_3;
defpred S2[ set , set ] means ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . $1 & dt `1 = $2 & dt in Union f );
A29: for k being Nat st k in Seg (len p) holds
ex x being Element of FinTrees the carrier of F1() st S2[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len p) implies ex x being Element of FinTrees the carrier of F1() st S2[k,x] )
assume k in Seg (len p) ; ::_thesis: ex x being Element of FinTrees the carrier of F1() st S2[k,x]
then A30: p . k in rng p by A28, FUNCT_1:def_3;
A31: rng p c= Union f by A26, A27, XBOOLE_1:1;
then p . k in Union f by A30;
then reconsider dt = p . k as Element of FinTrees [: the carrier of F1(),NAT:] by A7;
A32: dt `1 = (pr1 ( the carrier of F1(),NAT)) * dt by TREES_3:def_12;
A33: rng dt c= [: the carrier of F1(),NAT:] by RELAT_1:def_19;
dom (pr1 ( the carrier of F1(),NAT)) = [: the carrier of F1(),NAT:] by FUNCT_2:def_1;
then dom (dt `1) = dom dt by A32, A33, RELAT_1:27;
then reconsider x = dt `1 as Element of FinTrees the carrier of F1() by TREES_3:def_8;
take x ; ::_thesis: S2[k,x]
take dt ; ::_thesis: ( dt = p . k & dt `1 = x & dt in Union f )
thus ( dt = p . k & dt `1 = x & dt in Union f ) by A30, A31; ::_thesis: verum
end;
consider p1 being FinSequence of FinTrees the carrier of F1() such that
A34: dom p1 = Seg (len p) and
A35: for k being Nat st k in Seg (len p) holds
S2[k,p1 . k] from FINSEQ_1:sch_5(A29);
reconsider p = p as FinSequence of Trees [: the carrier of F1(),NAT:] by A23, Th1;
A36: dom (roots p1) = dom p1 by TREES_3:def_18;
A37: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def_12;
then A38: dom (pr1 (roots p)) = dom p1 by A28, A34, TREES_3:def_18;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p1_holds_
(roots_p1)_._k_=_(pr1_(roots_p))_._k
let k be Nat; ::_thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )
assume A39: k in dom p1 ; ::_thesis: (roots p1) . k = (pr1 (roots p)) . k
then consider dt being Element of FinTrees [: the carrier of F1(),NAT:] such that
A40: dt = p . k and
A41: dt `1 = p1 . k and
dt in Union f by A34, A35;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = p1 . k & (roots p1) . k = T . {} ) by A39, TREES_3:def_18;
then A42: (roots p1) . k = (dt . r) `1 by A41, TREES_3:39;
ex T being DecoratedTree st
( T = p . k & (roots p) . k = T . {} ) by A28, A34, A39, TREES_3:def_18;
hence (roots p1) . k = (pr1 (roots p)) . k by A37, A38, A39, A40, A42, MCART_1:def_12; ::_thesis: verum
end;
then A43: roots p1 = pr1 (roots p) by A36, A38, FINSEQ_1:13;
rng p1 c= TS F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p1 or x in TS F1() )
assume x in rng p1 ; ::_thesis: x in TS F1()
then consider k being set such that
A44: k in dom p1 and
A45: x = p1 . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A44;
ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A44;
hence x in TS F1() by A8, A12, A45; ::_thesis: verum
end;
then reconsider p1 = p1 as FinSequence of TS F1() by FINSEQ_1:def_4;
now__::_thesis:_for_t_being_DecoratedTree_of_the_carrier_of_F1()_st_t_in_rng_p1_holds_
P1[t]
let t be DecoratedTree of the carrier of F1(); ::_thesis: ( t in rng p1 implies P1[t] )
assume t in rng p1 ; ::_thesis: P1[t]
then consider k being set such that
A46: k in dom p1 and
A47: t = p1 . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A46;
A48: ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A46;
p . k in rng p by A28, A34, A46, FUNCT_1:def_3;
hence P1[t] by A19, A26, A47, A48; ::_thesis: verum
end;
then A49: P1[o -tree p1] by A2, A23, A43;
reconsider p1 = p1 as FinSequence of Trees the carrier of F1() by Th1;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
for_T_being_DecoratedTree_of_[:_the_carrier_of_F1(),NAT:]_st_T_=_p_._k_holds_
p1_._k_=_T_`1
let k be Element of NAT ; ::_thesis: ( k in dom p implies for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1 )
assume k in dom p ; ::_thesis: for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1
then ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A28, A35;
hence for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1 ; ::_thesis: verum
end;
hence contradiction by A21, A22, A28, A34, A49, TREES_4:27; ::_thesis: verum
end;
end;
A50: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A18);
let t be DecoratedTree of the carrier of F1(); ::_thesis: ( t in TS F1() implies P1[t] )
assume t in TS F1() ; ::_thesis: P1[t]
then consider tt being Element of FinTrees [: the carrier of F1(),NAT:] such that
A51: t = tt `1 and
A52: tt in Union f by A8, A12;
ex n being set st
( n in NAT & tt in f . n ) by A3, A52, CARD_5:2;
hence P1[t] by A50, A51; ::_thesis: verum
end;
scheme :: DTCONSTR:sch 8
DTConstrIndDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2() } :
ex f being Function of (TS F1()),F2() st
( ( for t being Symbol of F1() st t in Terminals F1() holds
f . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
f . (nt -tree ts) = F4(nt,(roots ts),(f * ts)) ) )
proof
set G = F1();
deffunc H3( Symbol of F1(), FinSequence) -> Element of F2() = F4($1,(pr1 (roots $2)),(pr2 (roots $2)));
deffunc H4( set , set ) -> set = $2 \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of F1(),F2():] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = { (root-tree [t,d]) where t is Symbol of F1(), d is Element of F2() : ( ( t in Terminals F1() & d = F3(t) ) or ( t ==> {} & d = F4(t,{},{}) ) ) } and
A3: for n being Nat holds f . (n + 1) = H4(n,f . n) from NAT_1:sch_11();
A4: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),F2():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
ex X1 being Subset of (FinTrees the carrier of F1()) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F1(),F2():] : t in Union f } & ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in X1 ) & ( for o being Symbol of F1()
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 F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) ) from DTCONSTR:sch_4(A1, A2, A4);
then A5: TS F1() = { (t `1) where t is Element of FinTrees [: the carrier of F1(),F2():] : t in Union f } by Def1;
defpred S1[ set , set ] means for dt being DecoratedTree of [: the carrier of F1(),F2():] st dt in Union f & $1 = dt `1 holds
$2 = (dt `2) . {};
A6: for e being set st e in TS F1() holds
ex u being set st
( u in F2() & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in TS F1() implies ex u being set st
( u in F2() & S1[e,u] ) )
assume e in TS F1() ; ::_thesis: ex u being set st
( u in F2() & S1[e,u] )
then consider DT being Element of FinTrees [: the carrier of F1(),F2():] such that
A7: e = DT `1 and
A8: DT in Union f by A5;
reconsider r = {} as Node of (DT `2) by TREES_1:22;
take u = (DT `2) . r; ::_thesis: ( u in F2() & S1[e,u] )
thus u in F2() ; ::_thesis: S1[e,u]
A9: for dt1, dt2 being DecoratedTree of [: the carrier of F1(),F2():] st dt1 in Union f & dt2 in Union f & dt1 `1 = dt2 `1 holds
dt1 = dt2 from DTCONSTR:sch_6(A1, A2, A4);
let dt be DecoratedTree of [: the carrier of F1(),F2():]; ::_thesis: ( dt in Union f & e = dt `1 implies u = (dt `2) . {} )
assume that
A10: dt in Union f and
A11: e = dt `1 ; ::_thesis: u = (dt `2) . {}
thus u = (dt `2) . {} by A7, A8, A9, A10, A11; ::_thesis: verum
end;
consider ff being Function such that
A12: ( dom ff = TS F1() & rng ff c= F2() ) and
A13: for e being set st e in TS F1() holds
S1[e,ff . e] from FUNCT_1:sch_5(A6);
reconsider ff = ff as Function of (TS F1()),F2() by A12, FUNCT_2:def_1, RELSET_1:4;
take ff ; ::_thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
ff . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ) )
consider X being Subset of (FinTrees [: the carrier of F1(),F2():]) such that
A14: X = Union f and
A15: for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,F3(d)] in X and
A16: for o being Symbol of F1()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X and
for F being Subset of (FinTrees [: the carrier of F1(),F2():]) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,F3(d)] in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F from DTCONSTR:sch_3(A1, A2, A4);
hereby ::_thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
let t be Symbol of F1(); ::_thesis: ( t in Terminals F1() implies ff . (root-tree t) = F3(t) )
assume A17: t in Terminals F1() ; ::_thesis: ff . (root-tree t) = F3(t)
A18: (root-tree [t,F3(t)]) `1 = root-tree t by TREES_4:25;
A19: (root-tree [t,F3(t)]) `2 = root-tree F3(t) by TREES_4:25;
root-tree [t,F3(t)] in Union f by A14, A15, A17;
then root-tree t in TS F1() by A5, A18;
hence ff . (root-tree t) = (root-tree F3(t)) . {} by A13, A14, A15, A17, A18, A19
.= F3(t) by TREES_4:3 ;
::_thesis: verum
end;
let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts implies ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) )
set rts = roots ts;
assume A20: nt ==> roots ts ; ::_thesis: ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
set x = ff * ts;
A21: dom ts = Seg (len ts) by FINSEQ_1:def_3;
defpred S2[ set , set ] means ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = $2 & dt `1 = ts . $1 & dt in Union f );
A22: for k being Nat st k in Seg (len ts) holds
ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] )
assume k in Seg (len ts) ; ::_thesis: ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x]
then A23: ts . k in rng ts by A21, FUNCT_1:def_3;
rng ts c= TS F1() by FINSEQ_1:def_4;
then ts . k in TS F1() by A23;
then ex x being Element of FinTrees [: the carrier of F1(),F2():] st
( ts . k = x `1 & x in Union f ) by A5;
hence ex x being Element of FinTrees [: the carrier of F1(),F2():] st S2[k,x] ; ::_thesis: verum
end;
consider dts being FinSequence of FinTrees [: the carrier of F1(),F2():] such that
A24: dom dts = Seg (len ts) and
A25: for k being Nat st k in Seg (len ts) holds
S2[k,dts . k] from FINSEQ_1:sch_5(A22);
rng dts c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng dts or x in X )
assume x in rng dts ; ::_thesis: x in X
then consider k being set such that
A26: k in dom ts and
A27: x = dts . k by A21, A24, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A26;
ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = x & dt `1 = ts . k & dt in Union f ) by A21, A25, A26, A27;
hence x in X by A14; ::_thesis: verum
end;
then reconsider dts = dts as FinSequence of X by FINSEQ_1:def_4;
A28: dom (roots ts) = dom ts by TREES_3:def_18;
A29: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def_12;
A30: dom (pr2 (roots dts)) = dom (roots dts) by MCART_1:def_13;
A31: dom (pr1 (roots dts)) = dom ts by A21, A24, A29, TREES_3:def_18;
A32: dom (pr2 (roots dts)) = dom ts by A21, A24, A30, TREES_3:def_18;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_
(roots_ts)_._k_=_(pr1_(roots_dts))_._k
let k be Nat; ::_thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A33: k in dom ts ; ::_thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that
A34: dt = dts . k and
A35: dt `1 = ts . k and
dt in Union f by A21, A25;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A33, TREES_3:def_18;
then A36: (roots ts) . k = (dt . r) `1 by A35, TREES_3:39;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A21, A24, A33, TREES_3:def_18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A29, A31, A33, A34, A36, MCART_1:def_12; ::_thesis: verum
end;
then A37: roots ts = pr1 (roots dts) by A28, A31, FINSEQ_1:13;
then A38: [nt,H3(nt,dts)] -tree dts in X by A16, A20;
A39: rng dts c= FinTrees [: the carrier of F1(),F2():] by FINSEQ_1:def_4;
FinTrees [: the carrier of F1(),F2():] c= Trees [: the carrier of F1(),F2():] by TREES_3:21;
then rng dts c= Trees [: the carrier of F1(),F2():] by A39, XBOOLE_1:1;
then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F1(),F2():] by FINSEQ_1:def_4;
A40: rng ts c= FinTrees the carrier of F1() by FINSEQ_1:def_4;
FinTrees the carrier of F1() c= Trees the carrier of F1() by TREES_3:21;
then rng ts c= Trees the carrier of F1() by A40, XBOOLE_1:1;
then reconsider ts9 = ts as FinSequence of Trees the carrier of F1() by FINSEQ_1:def_4;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_dts_holds_
for_T_being_DecoratedTree_of_[:_the_carrier_of_F1(),F2():]_st_T_=_dts_._i_holds_
ts_._i_=_T_`1
let i be Element of NAT ; ::_thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; ::_thesis: for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds
ts . i = T `1
then A41: ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = dts . i & dt `1 = ts . i & dt in Union f ) by A24, A25;
let T be DecoratedTree of [: the carrier of F1(),F2():]; ::_thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; ::_thesis: ts . i = T `1
hence ts . i = T `1 by A41; ::_thesis: verum
end;
then A42: ([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A21, A24, TREES_4:27;
A43: rng ts c= dom ff by A12, FINSEQ_1:def_4;
then A44: dom (ff * ts) = dom ts by RELAT_1:27;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_ts_holds_
(ff_*_ts)_._k_=_(pr2_(roots_dts))_._k
let k be Nat; ::_thesis: ( k in dom ts implies (ff * ts) . k = (pr2 (roots dts)) . k )
assume A45: k in dom ts ; ::_thesis: (ff * ts) . k = (pr2 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that
A46: dt = dts . k and
A47: dt `1 = ts . k and
A48: dt in Union f by A21, A25;
reconsider r = {} as Node of dt by TREES_1:22;
A49: ts . k in rng ts by A45, FUNCT_1:def_3;
A50: (ff * ts) . k = ff . (dt `1) by A44, A45, A47, FUNCT_1:12
.= (dt `2) . {} by A12, A13, A43, A47, A48, A49
.= (dt . r) `2 by TREES_3:39 ;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . r ) by A21, A24, A45, TREES_3:def_18;
hence (ff * ts) . k = (pr2 (roots dts)) . k by A29, A31, A45, A46, A50, MCART_1:def_13; ::_thesis: verum
end;
then A51: ff * ts = pr2 (roots dts) by A32, A44, FINSEQ_1:13;
reconsider r = {} as Node of ([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) by TREES_1:22;
nt -tree ts in TS F1() by A5, A14, A38, A42;
then ff . (nt -tree ts) = (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) `2) . r by A13, A14, A16, A20, A37, A42, A51
.= (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) . r) `2 by TREES_3:39
.= [nt,F4(nt,(roots ts),(ff * ts))] `2 by TREES_4:def_4 ;
hence ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ; ::_thesis: verum
end;
scheme :: DTCONSTR:sch 9
DTConstrUniqDef{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of (TS F1()),F2(), F6() -> Function of (TS F1()),F2() } :
F5() = F6()
provided
A1: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F5() . (nt -tree ts) = F4(nt,(roots ts),(F5() * ts)) ) ) and
A2: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F6() . (nt -tree ts) = F4(nt,(roots ts),(F6() * ts)) ) )
proof
set G = F1();
defpred S1[ set ] means F5() . $1 = F6() . $1;
A3: now__::_thesis:_for_s_being_Symbol_of_F1()_st_s_in_Terminals_F1()_holds_
S1[_root-tree_s]
let s be Symbol of F1(); ::_thesis: ( s in Terminals F1() implies S1[ root-tree s] )
assume A4: s in Terminals F1() ; ::_thesis: S1[ root-tree s]
then F5() . (root-tree s) = F3(s) by A1
.= F6() . (root-tree s) by A2, A4 ;
hence S1[ root-tree s] ; ::_thesis: verum
end;
A5: now__::_thesis:_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_
S1[t]_)_holds_
S1[nt_-tree_ts]
let nt be Symbol of F1(); ::_thesis: 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
S1[t] ) holds
S1[nt -tree ts]
let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of F1() st t in rng ts holds
S1[t] ; ::_thesis: S1[nt -tree ts]
A8: rng ts c= TS F1() by FINSEQ_1:def_4;
then rng ts c= dom F5() by FUNCT_2:def_1;
then A9: dom (F5() * ts) = dom ts by RELAT_1:27;
reconsider ntv1 = F5() * ts as FinSequence ;
reconsider ntv1 = ntv1 as FinSequence of F2() ;
rng ts c= dom F6() by A8, FUNCT_2:def_1;
then A10: dom (F6() * ts) = dom ts by RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_ts_holds_
(F5()_*_ts)_._x_=_(F6()_*_ts)_._x
let x be set ; ::_thesis: ( x in dom ts implies (F5() * ts) . x = (F6() * ts) . x )
assume A11: x in dom ts ; ::_thesis: (F5() * ts) . x = (F6() * ts) . x
then reconsider t = ts . x as Element of FinTrees the carrier of F1() by Th2;
t in rng ts by A11, FUNCT_1:def_3;
then A12: F5() . t = F6() . t by A7;
thus (F5() * ts) . x = F5() . t by A9, A11, FUNCT_1:12
.= (F6() * ts) . x by A10, A11, A12, FUNCT_1:12 ; ::_thesis: verum
end;
then A13: F5() * ts = F6() * ts by A9, A10, FUNCT_1:2;
F5() . (nt -tree ts) = F4(nt,(roots ts),ntv1) by A1, A6
.= F6() . (nt -tree ts) by A2, A6, A13 ;
hence S1[nt -tree ts] ; ::_thesis: verum
end;
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
S1[t] from DTCONSTR:sch_7(A3, A5);
then for x being set st x in TS F1() holds
F5() . x = F6() . x ;
hence F5() = F6() by FUNCT_2:12; ::_thesis: verum
end;
begin
defpred S1[ set , set ] means ( $1 = 1 & ( $2 = <*0*> or $2 = <*1*> ) );
definition
func PeanoNat -> non empty strict DTConstrStr means :Def2: :: DTCONSTR:def 2
( the carrier of it = {0,1} & ( for x being Symbol of it
for y being FinSequence of the carrier of it holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) );
existence
ex b1 being non empty strict DTConstrStr st
( the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) )
proof
thus ex G being non empty strict DTConstrStr st
( the carrier of G = {0,1} & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff S1[x,p] ) ) ) from DTCONSTR:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict DTConstrStr st the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) & the carrier of b2 = {0,1} & ( for x being Symbol of b2
for y being FinSequence of the carrier of b2 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) holds
b1 = b2
proof
thus for G1, G2 being non empty strict DTConstrStr st the carrier of G1 = {0,1} & ( for x being Symbol of G1
for p being FinSequence of the carrier of G1 holds
( x ==> p iff S1[x,p] ) ) & the carrier of G2 = {0,1} & ( for x being Symbol of G2
for p being FinSequence of the carrier of G2 holds
( x ==> p iff S1[x,p] ) ) holds
G1 = G2 from DTCONSTR:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines PeanoNat DTCONSTR:def_2_:_
for b1 being non empty strict DTConstrStr holds
( b1 = PeanoNat iff ( the carrier of b1 = {0,1} & ( for x being Symbol of b1
for y being FinSequence of the carrier of b1 holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ) );
set PN = PeanoNat ;
Lm2: the carrier of PeanoNat = {0,1}
by Def2;
then reconsider O = 0 , S = 1 as Symbol of PeanoNat by TARSKI:def_2;
Lm3: S ==> <*O*>
by Def2;
Lm4: S ==> <*S*>
by Def2;
Lm5: S ==> <*O*>
by Def2;
Lm6: S ==> <*S*>
by Def2;
Lm7: Terminals PeanoNat = { x where x is Symbol of PeanoNat : for tnt being FinSequence holds not x ==> tnt }
by LANG1:def_2;
Lm8: now__::_thesis:_for_x_being_FinSequence_holds_not_O_==>_x
given x being FinSequence such that A1: O ==> x ; ::_thesis: contradiction
[O,x] in the Rules of PeanoNat by A1, LANG1:def_1;
then x in the carrier of PeanoNat * by ZFMISC_1:87;
then x is FinSequence of the carrier of PeanoNat by FINSEQ_2:def_3;
hence contradiction by A1, Def2; ::_thesis: verum
end;
then Lm9: O in Terminals PeanoNat
by Lm7;
Lm10: Terminals PeanoNat c= {O}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Terminals PeanoNat or x in {O} )
assume x in Terminals PeanoNat ; ::_thesis: x in {O}
then consider y being Symbol of PeanoNat such that
A1: x = y and
A2: for tnt being FinSequence holds not y ==> tnt by Lm7;
( y = O or ( y = S & {O,S} <> {} ) ) by Lm2, TARSKI:def_2;
hence x in {O} by A1, A2, Lm5, TARSKI:def_1; ::_thesis: verum
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
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NonTerminals PeanoNat or x in {S} )
assume x in NonTerminals PeanoNat ; ::_thesis: x in {S}
then consider y being Symbol of PeanoNat such that
A1: x = y and
A2: ex tnt being FinSequence st y ==> tnt by Lm11;
( y = O or y = S ) by Lm2, TARSKI:def_2;
hence x in {S} by A1, A2, Lm8, TARSKI:def_1; ::_thesis: verum
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
definition
let G be non empty DTConstrStr ;
attrG is with_terminals means :Def3: :: DTCONSTR:def 3
Terminals G <> {} ;
attrG is with_nonterminals means :Def4: :: DTCONSTR:def 4
NonTerminals G <> {} ;
attrG is with_useful_nonterminals means :Def5: :: DTCONSTR:def 5
for nt being Symbol of G st nt in NonTerminals G holds
ex p being FinSequence of TS G st nt ==> roots p;
end;
:: deftheorem Def3 defines with_terminals DTCONSTR:def_3_:_
for G being non empty DTConstrStr holds
( G is with_terminals iff Terminals G <> {} );
:: deftheorem Def4 defines with_nonterminals DTCONSTR:def_4_:_
for G being non empty DTConstrStr holds
( G is with_nonterminals iff NonTerminals G <> {} );
:: deftheorem Def5 defines with_useful_nonterminals DTCONSTR:def_5_:_
for G being non empty DTConstrStr holds
( G is with_useful_nonterminals iff for nt being Symbol of G st nt in NonTerminals G holds
ex p being FinSequence of TS G st nt ==> roots p );
Lm16: ( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
proof
thus Terminals PeanoNat <> {} by Lm9; :: according to DTCONSTR:def_3 ::_thesis: ( PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
thus NonTerminals PeanoNat <> {} by Lm12; :: according to DTCONSTR:def_4 ::_thesis: PeanoNat is with_useful_nonterminals
reconsider rO = root-tree O as Element of TSPN by Def1, Lm9;
reconsider p = <*rO*> as FinSequence of TSPN ;
reconsider p = p as FinSequence of TS PeanoNat ;
let nt be Symbol of PeanoNat; :: according to DTCONSTR:def_5 ::_thesis: ( nt in NonTerminals PeanoNat implies ex p being FinSequence of TS PeanoNat st nt ==> roots p )
assume nt in NonTerminals PeanoNat ; ::_thesis: ex p being FinSequence of TS PeanoNat st nt ==> roots p
then A1: nt = S by Lm14, TARSKI:def_1;
take p ; ::_thesis: nt ==> roots p
A2: dom <*rO*> = Seg 1 by FINSEQ_1:38;
A3: dom <*O*> = Seg 1 by FINSEQ_1:38;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_
ex_rO_being_DecoratedTree_st_
(_rO_=_p_._i_&_<*O*>_._i_=_rO_._{}_)
let i be Element of NAT ; ::_thesis: ( i in dom p implies ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} ) )
assume A4: i in dom p ; ::_thesis: ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} )
reconsider rO = rO as DecoratedTree ;
take rO = rO; ::_thesis: ( rO = p . i & <*O*> . i = rO . {} )
A5: i = 1 by A2, A4, FINSEQ_1:2, TARSKI:def_1;
<*O*> . 1 = O by FINSEQ_1:40;
hence ( rO = p . i & <*O*> . i = rO . {} ) by A5, FINSEQ_1:40, TREES_4:3; ::_thesis: verum
end;
hence nt ==> roots p by A1, A2, A3, Lm5, TREES_3:def_18; ::_thesis: verum
end;
registration
cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals for DTConstrStr ;
existence
ex b1 being non empty DTConstrStr st
( b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict ) by Lm16;
end;
definition
let G be non empty with_terminals DTConstrStr ;
:: original: Terminals
redefine func Terminals G -> non empty Subset of G;
coherence
Terminals G is non empty Subset of G
proof
defpred S2[ Element of G] means for tnt being FinSequence holds not $1 ==> tnt;
{ t where t is Element of G : S2[t] } c= the carrier of G from FRAENKEL:sch_10();
hence Terminals G is non empty Subset of G by Def3, LANG1:def_2; ::_thesis: verum
end;
end;
registration
let G be non empty with_terminals DTConstrStr ;
cluster TS G -> non empty ;
coherence
not TS G is empty
proof
ex t being set st t in Terminals G by XBOOLE_0:def_1;
hence not TS G is empty by Def1; ::_thesis: verum
end;
end;
registration
let G be non empty with_useful_nonterminals DTConstrStr ;
cluster TS G -> non empty ;
coherence
not TS G is empty
proof
set s = the Symbol of G;
percases ( for tnt being FinSequence holds not the Symbol of G ==> tnt or ex tnt being FinSequence st the Symbol of G ==> tnt ) ;
suppose for tnt being FinSequence holds not the Symbol of G ==> tnt ; ::_thesis: not TS G is empty
then the Symbol of G in { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } ;
then the Symbol of G in Terminals G by LANG1:def_2;
hence not TS G is empty by Def1; ::_thesis: verum
end;
suppose ex tnt being FinSequence st the Symbol of G ==> tnt ; ::_thesis: not TS G is empty
then the Symbol of G in { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } ;
then the Symbol of G in NonTerminals G by LANG1:def_3;
then ex p being FinSequence of TS G st the Symbol of G ==> roots p by Def5;
hence not TS G is empty by Def1; ::_thesis: verum
end;
end;
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
defpred S2[ Element of G] means ex tnt being FinSequence st $1 ==> tnt;
{ t where t is Element of G : S2[t] } c= the carrier of G from FRAENKEL:sch_10();
hence NonTerminals G is non empty Subset of G by Def4, LANG1:def_3; ::_thesis: verum
end;
end;
definition
let G be non empty with_terminals DTConstrStr ;
mode Terminal of G is Element of Terminals G;
end;
definition
let G be non empty with_nonterminals DTConstrStr ;
mode NonTerminal of G is Element of NonTerminals G;
end;
definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
mode SubtreeSeq of nt -> FinSequence of TS G means :Def6: :: DTCONSTR:def 6
nt ==> roots it;
existence
ex b1 being FinSequence of TS G st nt ==> roots b1 by Def5;
end;
:: deftheorem Def6 defines SubtreeSeq DTCONSTR:def_6_:_
for G being non empty with_nonterminals with_useful_nonterminals DTConstrStr
for nt being NonTerminal of G
for b3 being FinSequence of TS G holds
( b3 is SubtreeSeq of nt iff nt ==> roots b3 );
definition
let G be non empty with_terminals DTConstrStr ;
let t be Terminal of G;
:: original: root-tree
redefine func root-tree t -> Element of TS G;
coherence
root-tree t is Element of TS G by Def1;
end;
definition
let G be non empty with_nonterminals with_useful_nonterminals DTConstrStr ;
let nt be NonTerminal of G;
let p be SubtreeSeq of nt;
:: original: -tree
redefine funcnt -tree p -> Element of TS G;
coherence
nt -tree p is Element of TS G
proof
nt ==> roots p by Def6;
hence nt -tree p is Element of TS G by Def1; ::_thesis: verum
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
let G be non empty with_terminals DTConstrStr ; ::_thesis: for tsg being Element of TS G
for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
let tsg be Element of TS G; ::_thesis: for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
let s be Terminal of G; ::_thesis: ( tsg . {} = s implies tsg = root-tree s )
assume A1: tsg . {} = s ; ::_thesis: tsg = root-tree s
defpred S2[ DecoratedTree of the carrier of G] means for s being Terminal of G st $1 . {} = s holds
$1 = root-tree s;
A2: for s being Symbol of G st s in Terminals G holds
S2[ root-tree s] by TREES_4:3;
A3: now__::_thesis:_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_G_st_t_in_rng_ts_holds_
S2[t]_)_holds_
S2[nt_-tree_ts]
let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A4: nt ==> roots ts and
for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ; ::_thesis: S2[nt -tree ts]
thus S2[nt -tree ts] ::_thesis: verum
proof
let s be Terminal of G; ::_thesis: ( (nt -tree ts) . {} = s implies nt -tree ts = root-tree s )
assume A5: (nt -tree ts) . {} = s ; ::_thesis: nt -tree ts = root-tree s
A6: (nt -tree ts) . {} = nt by TREES_4:def_4;
A7: s in Terminals G ;
Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def_2;
then ex t being Symbol of G st
( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A7;
hence nt -tree ts = root-tree s by A4, A5, A6; ::_thesis: verum
end;
end;
for t being DecoratedTree of the carrier of G st t in TS G holds
S2[t] from DTCONSTR:sch_7(A2, A3);
hence tsg = root-tree s by A1; ::_thesis: verum
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
let G be non empty with_terminals with_nonterminals DTConstrStr ; ::_thesis: 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 )
defpred S2[ DecoratedTree of the carrier of G] means for nt being NonTerminal of G st $1 . {} = nt holds
ex ts being FinSequence of TS G st
( $1 = nt -tree ts & nt ==> roots ts );
A1: now__::_thesis:_for_s_being_Symbol_of_G_st_s_in_Terminals_G_holds_
S2[_root-tree_s]
let s be Symbol of G; ::_thesis: ( s in Terminals G implies S2[ root-tree s] )
assume A2: s in Terminals G ; ::_thesis: S2[ root-tree s]
thus S2[ root-tree s] ::_thesis: verum
proof
let nt be NonTerminal of G; ::_thesis: ( (root-tree s) . {} = nt implies ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts ) )
assume (root-tree s) . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts )
then A3: s = nt by TREES_4:3;
Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def_2;
then A4: ex t being Symbol of G st
( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A2;
A5: nt in NonTerminals G ;
NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def_3;
then ex t being Symbol of G st
( nt = t & ex tnt being FinSequence st t ==> tnt ) by A5;
hence ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts ) by A3, A4; ::_thesis: verum
end;
end;
A6: now__::_thesis:_for_nnt_being_Symbol_of_G
for_tts_being_FinSequence_of_TS_G_st_nnt_==>_roots_tts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_G_st_t_in_rng_tts_holds_
S2[t]_)_holds_
S2[nnt_-tree_tts]
let nnt be Symbol of G; ::_thesis: for tts being FinSequence of TS G st nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ) holds
S2[nnt -tree tts]
let tts be FinSequence of TS G; ::_thesis: ( nnt ==> roots tts & ( for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ) implies S2[nnt -tree tts] )
assume that
A7: nnt ==> roots tts and
for t being DecoratedTree of the carrier of G st t in rng tts holds
S2[t] ; ::_thesis: S2[nnt -tree tts]
thus S2[nnt -tree tts] ::_thesis: verum
proof
let nt be NonTerminal of G; ::_thesis: ( (nnt -tree tts) . {} = nt implies ex ts being FinSequence of TS G st
( nnt -tree tts = nt -tree ts & nt ==> roots ts ) )
assume A8: (nnt -tree tts) . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st
( nnt -tree tts = nt -tree ts & nt ==> roots ts )
take ts = tts; ::_thesis: ( nnt -tree tts = nt -tree ts & nt ==> roots ts )
thus ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) by A7, A8, TREES_4:def_4; ::_thesis: verum
end;
end;
A9: for t being DecoratedTree of the carrier of G st t in TS G holds
S2[t] from DTCONSTR:sch_7(A1, A6);
let tsg be Element of TS G; ::_thesis: 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 )
let nt be NonTerminal of G; ::_thesis: ( tsg . {} = nt implies ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts ) )
assume tsg . {} = nt ; ::_thesis: ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts )
hence ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts ) by A9; ::_thesis: verum
end;
begin
registration
cluster PeanoNat -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
( PeanoNat is with_terminals & PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals ) by Lm16;
end;
set PN = PeanoNat ;
reconsider O = O as Terminal of PeanoNat by Lm9;
reconsider S = S as NonTerminal of PeanoNat by Lm12;
definition
let nt be NonTerminal of PeanoNat;
let t be Element of TS PeanoNat;
:: original: -tree
redefine funcnt -tree t -> Element of TS PeanoNat;
coherence
nt -tree t is Element of TS PeanoNat
proof
reconsider r = {} as Node of t by TREES_1:22;
( t . r = 0 or t . r = 1 ) by Lm2, TARSKI:def_2;
then A1: ( roots <*t*> = <*0*> or roots <*t*> = <*1*> ) by Th4;
nt = S by Lm15, TARSKI:def_1;
then nt -tree <*t*> in TS PeanoNat by A1, Def1, Lm5, Lm6;
hence nt -tree t is Element of TS PeanoNat by TREES_4:def_5; ::_thesis: verum
end;
end;
definition
let x be FinSequence of NAT ;
func plus-one x -> Element of NAT equals :: DTCONSTR:def 7
(x . 1) + 1;
coherence
(x . 1) + 1 is Element of NAT ;
end;
:: deftheorem defines plus-one DTCONSTR:def_7_:_
for x being FinSequence of NAT holds plus-one x = (x . 1) + 1;
deffunc H3( set , set , FinSequence of NAT ) -> Element of NAT = plus-one $3;
definition
func PN-to-NAT -> Function of (TS PeanoNat),NAT means :Def8: :: DTCONSTR:def 8
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it . (nt -tree ts) = plus-one (it * ts) ) );
existence
ex b1 being Function of (TS PeanoNat),NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) )
proof
thus ex f being Function of (TS PeanoNat),NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = H1(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
f . (nt -tree ts) = H3(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (TS PeanoNat),NAT st ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b2 . (nt -tree ts) = plus-one (b2 * ts) ) holds
b1 = b2
proof
let it1, it2 be Function of (TS PeanoNat),NAT; ::_thesis: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it1 . (nt -tree ts) = plus-one (it1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it2 . (nt -tree ts) = plus-one (it2 * ts) ) implies it1 = it2 )
assume that
A1: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it1 . (root-tree t) = H1(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it1 . (nt -tree ts) = H3(nt, roots ts,it1 * ts) ) ) and
A2: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it2 . (root-tree t) = H1(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it2 . (nt -tree ts) = H3(nt, roots ts,it2 * ts) ) ) ; ::_thesis: it1 = it2
thus it1 = it2 from DTCONSTR:sch_9(A1, A2); ::_thesis: verum
end;
end;
:: deftheorem Def8 defines PN-to-NAT DTCONSTR:def_8_:_
for b1 being Function of (TS PeanoNat),NAT holds
( b1 = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b1 . (nt -tree ts) = plus-one (b1 * ts) ) ) );
definition
let x be Element of TS PeanoNat;
func PNsucc x -> Element of TS PeanoNat equals :: DTCONSTR:def 9
1 -tree <*x*>;
coherence
1 -tree <*x*> is Element of TS PeanoNat
proof
reconsider r = {} as Node of x by TREES_1:22;
A1: roots <*x*> = <*(x . r)*> by Th4;
( x . r = O or x . r = S ) by Lm2, TARSKI:def_2;
hence 1 -tree <*x*> is Element of TS PeanoNat by A1, Def1, Lm5, Lm6; ::_thesis: verum
end;
end;
:: deftheorem defines PNsucc DTCONSTR:def_9_:_
for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>;
deffunc H4( set , Element of TS PeanoNat) -> Element of TS PeanoNat = PNsucc $2;
definition
func NAT-to-PN -> Function of NAT,(TS PeanoNat) means :Def10: :: DTCONSTR:def 10
( it . 0 = root-tree 0 & ( for n being Nat holds it . (n + 1) = PNsucc (it . n) ) );
existence
ex b1 being Function of NAT,(TS PeanoNat) st
( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) )
proof
ex f being Function of NAT,(TS PeanoNat) st
( f . 0 = root-tree O & ( for n being Nat holds f . (n + 1) = H4(n,f . n) ) ) from NAT_1:sch_12();
hence ex b1 being Function of NAT,(TS PeanoNat) st
( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of NAT,(TS PeanoNat) st b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) & b2 . 0 = root-tree 0 & ( for n being Nat holds b2 . (n + 1) = PNsucc (b2 . n) ) holds
b1 = b2
proof
let it1, it2 be Function of NAT,(TS PeanoNat); ::_thesis: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) implies it1 = it2 )
assume A1: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) & not it1 = it2 ) ; ::_thesis: contradiction
then A2: it1 . 0 = root-tree O ;
A3: for n being Nat holds it1 . (n + 1) = H4(n,it1 . n) by A1;
A4: it2 . 0 = root-tree O by A1;
A5: for n being Nat holds it2 . (n + 1) = H4(n,it2 . n) by A1;
it1 = it2 from NAT_1:sch_16(A2, A3, A4, A5);
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines NAT-to-PN DTCONSTR:def_10_:_
for b1 being Function of NAT,(TS PeanoNat) holds
( b1 = NAT-to-PN iff ( b1 . 0 = root-tree 0 & ( for n being Nat holds b1 . (n + 1) = PNsucc (b1 . n) ) ) );
theorem :: DTCONSTR:11
for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)
proof
defpred S2[ DecoratedTree of the carrier of PeanoNat] means $1 = NAT-to-PN . (PN-to-NAT . $1);
A1: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_
S2[_root-tree_s]
let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] )
assume A2: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s]
then NAT-to-PN . (PN-to-NAT . (root-tree s)) = NAT-to-PN . 0 by Def8
.= root-tree O by Def10 ;
hence S2[ root-tree s] by A2, Lm10, TARSKI:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat
for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_
S2[t]_)_holds_
S2[nt_-tree_ts]
let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; ::_thesis: S2[nt -tree ts]
A6: nt <> O by A4, Lm8;
( roots ts = <*O*> or roots ts = <*S*> ) by A4, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider dt being Element of FinTrees the carrier of PeanoNat such that
A7: ts = <*dt*> and
A8: dt in TS PeanoNat by Th5;
reconsider dt = dt as Element of TS PeanoNat by A8;
rng ts = {dt} by A7, FINSEQ_1:38;
then dt in rng ts by TARSKI:def_1;
then A9: dt = NAT-to-PN . (PN-to-NAT . dt) by A5;
A10: PN-to-NAT * ts = <*(PN-to-NAT . dt)*> by A7, FINSEQ_2:35;
set N = PN-to-NAT . dt;
A11: plus-one <*(PN-to-NAT . dt)*> = (PN-to-NAT . dt) + 1 by FINSEQ_1:40;
NAT-to-PN . ((PN-to-NAT . dt) + 1) = PNsucc dt by A9, Def10
.= nt -tree ts by A6, A7, Lm2, TARSKI:def_2 ;
hence S2[nt -tree ts] by A4, A10, A11, Def8; ::_thesis: verum
end;
for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch_7(A1, A3);
hence for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn) ; ::_thesis: verum
end;
Lm17: 0 = PN-to-NAT . (root-tree O) by Def8
.= PN-to-NAT . (NAT-to-PN . 0) by Def10 ;
Lm18: now__::_thesis:_for_n_being_Element_of_NAT_st_n_=_PN-to-NAT_._(NAT-to-PN_._n)_holds_
n_+_1_=_PN-to-NAT_._(NAT-to-PN_._(n_+_1))
let n be Element of NAT ; ::_thesis: ( n = PN-to-NAT . (NAT-to-PN . n) implies n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) )
assume A1: n = PN-to-NAT . (NAT-to-PN . n) ; ::_thesis: n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1))
reconsider dt = NAT-to-PN . n as Element of TS PeanoNat ;
reconsider r = {} as Node of dt by TREES_1:22;
A2: ( dt . r = O or dt . r = S ) by Lm2, TARSKI:def_2;
A3: NAT-to-PN . (n + 1) = PNsucc (NAT-to-PN . n) by Def10
.= S -tree <*(NAT-to-PN . n)*> ;
A4: S ==> roots <*(NAT-to-PN . n)*> by A2, Lm3, Lm4, Th4;
<*(PN-to-NAT . (NAT-to-PN . n))*> = PN-to-NAT * <*(NAT-to-PN . n)*> by FINSEQ_2:35;
then PN-to-NAT . (S -tree <*(NAT-to-PN . n)*>) = plus-one <*n*> by A1, A4, Def8
.= n + 1 by FINSEQ_1:40 ;
hence n + 1 = PN-to-NAT . (NAT-to-PN . (n + 1)) by A3; ::_thesis: verum
end;
theorem :: DTCONSTR:12
for n being Element of NAT holds n = PN-to-NAT . (NAT-to-PN . n)
proof
defpred S2[ Element of NAT ] means $1 = PN-to-NAT . (NAT-to-PN . $1);
A1: S2[ 0 ] by Lm17;
A2: for n being Element of NAT st S2[n] holds
S2[n + 1] by Lm18;
thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A1, A2); ::_thesis: verum
end;
begin
definition
let G be non empty DTConstrStr ;
let tsg be DecoratedTree of the carrier of G;
assume A1: tsg in TS G ;
defpred S2[ set ] means $1 in Terminals G;
deffunc H5( set ) -> set = <*$1*>;
deffunc H6( set ) -> set = {} ;
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
(_(_S2[x]_implies_H5(x)_in_(Terminals_G)_*_)_&_(_not_S2[x]_implies_H6(x)_in_(Terminals_G)_*_)_)
let x be set ; ::_thesis: ( x in the carrier of G implies ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) ) )
assume x in the carrier of G ; ::_thesis: ( ( S2[x] implies H5(x) in (Terminals G) * ) & ( not S2[x] implies H6(x) in (Terminals G) * ) )
hereby ::_thesis: ( not S2[x] implies H6(x) in (Terminals G) * )
assume A3: S2[x] ; ::_thesis: H5(x) in (Terminals G) *
then reconsider T = Terminals G as non empty set ;
reconsider x9 = x as Element of T by A3;
<*x9*> is FinSequence of T ;
hence H5(x) in (Terminals G) * ; ::_thesis: verum
end;
assume not S2[x] ; ::_thesis: H6(x) in (Terminals G) *
<*> (Terminals G) = {} ;
hence H6(x) in (Terminals G) * ; ::_thesis: verum
end;
consider s2t being Function of the carrier of G,((Terminals G) *) such that
A4: for s being set st s in the carrier of G holds
( ( S2[s] implies s2t . s = H5(s) ) & ( not S2[s] implies s2t . s = H6(s) ) ) from FUNCT_2:sch_5(A2);
deffunc H7( Symbol of G) -> Element of (Terminals G) * = s2t . $1;
deffunc H8( set , set , FinSequence of (Terminals G) * ) -> Element of (Terminals G) * = FlattenSeq $3;
deffunc H9( set ) -> set = <*$1*>;
func TerminalString tsg -> FinSequence of Terminals G means :Def11: :: DTCONSTR:def 11
ex f being Function of (TS G),((Terminals G) *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) );
existence
ex b1 being FinSequence of Terminals G ex f being Function of (TS G),((Terminals G) *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )
proof
consider f being Function of (TS G),((Terminals G) *) such that
A5: ( ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = H7(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = H8(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8();
f . tsg is Element of (Terminals G) * by A1, FUNCT_2:5;
then reconsider IT = f . tsg as FinSequence of Terminals G ;
take IT ; ::_thesis: 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) ) )
take f ; ::_thesis: ( 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) ) )
thus IT = f . tsg ; ::_thesis: ( ( 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) ) )
hereby ::_thesis: 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)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> )
assume A6: t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*>
then f . (root-tree t) = s2t . t by A5;
hence f . (root-tree t) = <*t*> by A4, A6; ::_thesis: verum
end;
thus 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) by A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of Terminals G st ex f being Function of (TS G),((Terminals G) *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) & ex f being Function of (TS G),((Terminals G) *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) holds
b1 = b2
proof
let it1, it2 be FinSequence of Terminals G; ::_thesis: ( ex f being Function of (TS G),((Terminals G) *) st
( it1 = 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
( it2 = 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) ) ) implies it1 = it2 )
given f1 being Function of (TS G),((Terminals G) *) such that A7: it1 = f1 . tsg and
A8: for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = <*t*> and
A9: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = FlattenSeq (f1 * ts) ; ::_thesis: ( for f being Function of (TS G),((Terminals G) *) holds
( not it2 = f . tsg or ex t being Symbol of G st
( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G st
( nt ==> roots ts & not f . (nt -tree ts) = FlattenSeq (f * ts) ) ) or it1 = it2 )
given f2 being Function of (TS G),((Terminals G) *) such that A10: it2 = f2 . tsg and
A11: for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = <*t*> and
A12: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = FlattenSeq (f2 * ts) ; ::_thesis: it1 = it2
A13: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f1_._(root-tree_t)_=_H7(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f1_._(nt_-tree_ts)_=_H8(nt,_roots_ts,f1_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H8(nt, roots ts,f1 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H7(t) )
assume A14: t in Terminals G ; ::_thesis: f1 . (root-tree t) = H7(t)
hence f1 . (root-tree t) = <*t*> by A8
.= H7(t) by A4, A14 ;
::_thesis: verum
end;
thus for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H8(nt, roots ts,f1 * ts) by A9; ::_thesis: verum
end;
A15: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f2_._(root-tree_t)_=_H7(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f2_._(nt_-tree_ts)_=_H8(nt,_roots_ts,f2_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H8(nt, roots ts,f2 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H7(t) )
assume A16: t in Terminals G ; ::_thesis: f2 . (root-tree t) = H7(t)
hence f2 . (root-tree t) = <*t*> by A11
.= H7(t) by A4, A16 ;
::_thesis: verum
end;
thus for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H8(nt, roots ts,f2 * ts) by A12; ::_thesis: verum
end;
f1 = f2 from DTCONSTR:sch_9(A13, A15);
hence it1 = it2 by A7, A10; ::_thesis: verum
end;
A17: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
H9(x)_in_the_carrier_of_G_*
let x be set ; ::_thesis: ( x in the carrier of G implies H9(x) in the carrier of G * )
assume x in the carrier of G ; ::_thesis: H9(x) in the carrier of G *
then reconsider x9 = x as Element of G ;
<*x9*> is FinSequence of the carrier of G ;
hence H9(x) in the carrier of G * ; ::_thesis: verum
end;
consider s2s being Function of the carrier of G,( the carrier of G *) such that
A18: for s being set st s in the carrier of G holds
s2s . s = H9(s) from FUNCT_2:sch_2(A17);
deffunc H10( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H11( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3);
func PreTraversal tsg -> FinSequence of the carrier of G means :Def12: :: DTCONSTR:def 12
ex f being Function of (TS G),( the carrier of G *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) );
existence
ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) )
proof
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) ^ (FlattenSeq $3);
consider f being Function of (TS G),( the carrier of G *) such that
A19: ( ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = H12(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = H13(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8();
f . tsg is Element of the carrier of G * by A1, FUNCT_2:5;
then reconsider IT = f . tsg as FinSequence of the carrier of G ;
take IT ; ::_thesis: 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) ) )
take f ; ::_thesis: ( 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) ) )
thus IT = f . tsg ; ::_thesis: ( ( 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) ) )
hereby ::_thesis: 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)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> )
assume t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*>
then f . (root-tree t) = s2s . t by A19;
hence f . (root-tree t) = <*t*> by A18; ::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: 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)
let ts be FinSequence of TS G; ::_thesis: 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)
let rts be FinSequence; ::_thesis: ( rts = roots ts & nt ==> rts implies for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) )
assume that
A20: rts = roots ts and
A21: nt ==> rts ; ::_thesis: for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x)
let x be FinSequence of the carrier of G * ; ::_thesis: ( x = f * ts implies f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) )
assume x = f * ts ; ::_thesis: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x)
hence f . (nt -tree ts) = (s2s . nt) ^ (FlattenSeq x) by A19, A20, A21
.= <*nt*> ^ (FlattenSeq x) by A18 ;
::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) & ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) holds
b1 = b2
proof
let it1, it2 be FinSequence of the carrier of G; ::_thesis: ( ex f being Function of (TS G),( the carrier of G *) st
( it1 = 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
( it2 = 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) ) ) implies it1 = it2 )
given f1 being Function of (TS G),( the carrier of G *) such that A22: it1 = f1 . tsg and
A23: for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = <*t*> and
A24: 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 = f1 * ts holds
f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; ::_thesis: ( for f being Function of (TS G),( the carrier of G *) holds
( not it2 = f . tsg or ex t being Symbol of G st
( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G ex rts being FinSequence st
( rts = roots ts & nt ==> rts & ex x being FinSequence of the carrier of G * st
( x = f * ts & not f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) ) or it1 = it2 )
given f2 being Function of (TS G),( the carrier of G *) such that A25: it2 = f2 . tsg and
A26: for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = <*t*> and
A27: 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 = f2 * ts holds
f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; ::_thesis: it1 = it2
A28: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f1_._(root-tree_t)_=_H10(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f1_._(nt_-tree_ts)_=_H11(nt,_roots_ts,f1_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H10(t) )
assume t in Terminals G ; ::_thesis: f1 . (root-tree t) = H10(t)
hence f1 . (root-tree t) = <*t*> by A23
.= H10(t) by A18 ;
::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts)
let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts) )
assume nt ==> roots ts ; ::_thesis: f1 . (nt -tree ts) = H11(nt, roots ts,f1 * ts)
hence f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f1 * ts)) by A24
.= H11(nt, roots ts,f1 * ts) by A18 ;
::_thesis: verum
end;
A29: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f2_._(root-tree_t)_=_H10(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f2_._(nt_-tree_ts)_=_H11(nt,_roots_ts,f2_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H10(t) )
assume t in Terminals G ; ::_thesis: f2 . (root-tree t) = H10(t)
hence f2 . (root-tree t) = <*t*> by A26
.= H10(t) by A18 ;
::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts)
let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts) )
assume nt ==> roots ts ; ::_thesis: f2 . (nt -tree ts) = H11(nt, roots ts,f2 * ts)
hence f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f2 * ts)) by A27
.= H11(nt, roots ts,f2 * ts) by A18 ;
::_thesis: verum
end;
f1 = f2 from DTCONSTR:sch_9(A28, A29);
hence it1 = it2 by A22, A25; ::_thesis: verum
end;
deffunc H12( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H13( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (FlattenSeq $3) ^ (s2s . $1);
func PostTraversal tsg -> FinSequence of the carrier of G means :Def13: :: DTCONSTR:def 13
ex f being Function of (TS G),( the carrier of G *) st
( it = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) );
existence
ex b1 being FinSequence of the carrier of G ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
proof
consider f being Function of (TS G),( the carrier of G *) such that
A30: ( ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = H12(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = H13(nt, roots ts,f * ts) ) ) from DTCONSTR:sch_8();
f . tsg is Element of the carrier of G * by A1, FUNCT_2:5;
then reconsider IT = f . tsg as FinSequence of the carrier of G ;
take IT ; ::_thesis: 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*> ) )
take f ; ::_thesis: ( 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*> ) )
thus IT = f . tsg ; ::_thesis: ( ( 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*> ) )
hereby ::_thesis: 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*>
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> )
assume t in Terminals G ; ::_thesis: f . (root-tree t) = <*t*>
then f . (root-tree t) = s2s . t by A30;
hence f . (root-tree t) = <*t*> by A18; ::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: 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*>
let ts be FinSequence of TS G; ::_thesis: 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*>
let rts be FinSequence; ::_thesis: ( rts = roots ts & nt ==> rts implies for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> )
assume that
A31: rts = roots ts and
A32: nt ==> rts ; ::_thesis: for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
let x be FinSequence of the carrier of G * ; ::_thesis: ( x = f * ts implies f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> )
assume x = f * ts ; ::_thesis: f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
hence f . (nt -tree ts) = (FlattenSeq x) ^ (s2s . nt) by A30, A31, A32
.= (FlattenSeq x) ^ <*nt*> by A18 ;
::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st ex f being Function of (TS G),( the carrier of G *) st
( b1 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) & ex f being Function of (TS G),( the carrier of G *) st
( b2 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) holds
b1 = b2
proof
let it1, it2 be FinSequence of the carrier of G; ::_thesis: ( ex f being Function of (TS G),( the carrier of G *) st
( it1 = 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
( it2 = 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*> ) ) implies it1 = it2 )
given f1 being Function of (TS G),( the carrier of G *) such that A33: it1 = f1 . tsg and
A34: for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = <*t*> and
A35: 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 = f1 * ts holds
f1 . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ; ::_thesis: ( for f being Function of (TS G),( the carrier of G *) holds
( not it2 = f . tsg or ex t being Symbol of G st
( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G ex rts being FinSequence st
( rts = roots ts & nt ==> rts & ex x being FinSequence of the carrier of G * st
( x = f * ts & not f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) ) or it1 = it2 )
given f2 being Function of (TS G),( the carrier of G *) such that A36: it2 = f2 . tsg and
A37: for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = <*t*> and
A38: 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 = f2 * ts holds
f2 . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ; ::_thesis: it1 = it2
A39: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f1_._(root-tree_t)_=_H12(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f1_._(nt_-tree_ts)_=_H13(nt,_roots_ts,f1_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f1 . (root-tree t) = H12(t) )
assume t in Terminals G ; ::_thesis: f1 . (root-tree t) = H12(t)
hence f1 . (root-tree t) = <*t*> by A34
.= H12(t) by A18 ;
::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts)
let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts) )
assume nt ==> roots ts ; ::_thesis: f1 . (nt -tree ts) = H13(nt, roots ts,f1 * ts)
hence f1 . (nt -tree ts) = (FlattenSeq (f1 * ts)) ^ <*nt*> by A35
.= H13(nt, roots ts,f1 * ts) by A18 ;
::_thesis: verum
end;
A40: now__::_thesis:_(_(_for_t_being_Symbol_of_G_st_t_in_Terminals_G_holds_
f2_._(root-tree_t)_=_H12(t)_)_&_(_for_nt_being_Symbol_of_G
for_ts_being_FinSequence_of_TS_G_st_nt_==>_roots_ts_holds_
f2_._(nt_-tree_ts)_=_H13(nt,_roots_ts,f2_*_ts)_)_)
hereby ::_thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts)
let t be Symbol of G; ::_thesis: ( t in Terminals G implies f2 . (root-tree t) = H12(t) )
assume t in Terminals G ; ::_thesis: f2 . (root-tree t) = H12(t)
hence f2 . (root-tree t) = <*t*> by A37
.= H12(t) by A18 ;
::_thesis: verum
end;
let nt be Symbol of G; ::_thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts)
let ts be FinSequence of TS G; ::_thesis: ( nt ==> roots ts implies f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts) )
assume nt ==> roots ts ; ::_thesis: f2 . (nt -tree ts) = H13(nt, roots ts,f2 * ts)
hence f2 . (nt -tree ts) = (FlattenSeq (f2 * ts)) ^ <*nt*> by A38
.= H13(nt, roots ts,f2 * ts) by A18 ;
::_thesis: verum
end;
f1 = f2 from DTCONSTR:sch_9(A39, A40);
hence it1 = it2 by A33, A36; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines TerminalString DTCONSTR:def_11_:_
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of Terminals G holds
( b3 = TerminalString tsg iff ex f being Function of (TS G),((Terminals G) *) st
( b3 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) );
:: deftheorem Def12 defines PreTraversal DTCONSTR:def_12_:_
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PreTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st
( b3 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) );
:: deftheorem Def13 defines PostTraversal DTCONSTR:def_13_:_
for G being non empty DTConstrStr
for tsg being DecoratedTree of the carrier of G st tsg in TS G holds
for b3 being FinSequence of the carrier of G holds
( b3 = PostTraversal tsg iff ex f being Function of (TS G),( the carrier of G *) st
( b3 = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) ) );
definition
let G be non empty with_nonterminals DTConstrStr ;
let nt be Symbol of G;
func TerminalLanguage nt -> Subset of ((Terminals G) *) equals :: DTCONSTR:def 14
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *)
proof
set TL = { (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 ) } c= (Terminals G) *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in (Terminals G) * )
assume x in { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in (Terminals G) *
then ex tsg being Element of FinTrees the carrier of G st
( x = TerminalString tsg & tsg in TS G & tsg . {} = nt ) ;
hence x in (Terminals G) * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ((Terminals G) *) ; ::_thesis: verum
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
set TL = { (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 ) } c= the carrier of G *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in the carrier of G * )
assume x in { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in the carrier of G *
then ex tsg being Element of FinTrees the carrier of G st
( x = PreTraversal tsg & tsg in TS G & tsg . {} = nt ) ;
hence x in the carrier of G * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence { (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 *) ; ::_thesis: verum
end;
func PostTraversalLanguage nt -> Subset of ( the carrier of G *) equals :: DTCONSTR:def 16
{ (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
coherence
{ (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } is Subset of ( the carrier of G *)
proof
set TL = { (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 ) } c= the carrier of G *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } or x in the carrier of G * )
assume x in { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ; ::_thesis: x in the carrier of G *
then ex tsg being Element of FinTrees the carrier of G st
( x = PostTraversal tsg & tsg in TS G & tsg . {} = nt ) ;
hence x in the carrier of G * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence { (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 *) ; ::_thesis: verum
end;
end;
:: deftheorem defines TerminalLanguage DTCONSTR:def_14_:_
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds TerminalLanguage nt = { (TerminalString tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
:: deftheorem defines PreTraversalLanguage DTCONSTR:def_15_:_
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds PreTraversalLanguage nt = { (PreTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
:: deftheorem defines PostTraversalLanguage DTCONSTR:def_16_:_
for G being non empty with_nonterminals DTConstrStr
for nt being Symbol of G holds PostTraversalLanguage nt = { (PostTraversal tsg) where tsg is Element of FinTrees the carrier of G : ( tsg in TS G & tsg . {} = nt ) } ;
theorem Th13: :: DTCONSTR:13
for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
TerminalString t = <*0*>
proof
consider f being Function of (TS PeanoNat),((Terminals PeanoNat) *) such that
A1: TerminalString (root-tree O) = f . (root-tree O) and
A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = <*t*> and
A3: for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) by Def11;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means TerminalString $1 = <*0*>;
A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_
S2[_root-tree_s]
let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] )
assume s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s]
then s = O by Lm10, TARSKI:def_1;
hence S2[ root-tree s] by A1, A2; ::_thesis: verum
end;
A5: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat
for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_
S2[t]_)_holds_
S2[nt_-tree_ts]
let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A6: nt ==> roots ts and
A7: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; ::_thesis: S2[nt -tree ts]
A8: nt -tree ts in TS PeanoNat by A6, Def1;
( roots ts = <*O*> or roots ts = <*1*> ) by A6, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A9: ts = <*x*> and
A10: x in TS PeanoNat by Th5;
reconsider x9 = x as Element of TS PeanoNat by A10;
rng ts = {x} by A9, FINSEQ_1:39;
then A11: x in rng ts by TARSKI:def_1;
f . x9 is Element of (Terminals PeanoNat) * ;
then A12: f . x9 = TerminalString x by A2, A3, Def11
.= <*O*> by A7, A11 ;
f * ts = <*(f . x)*> by A9, FINSEQ_2:35;
then f . (nt -tree ts) = FlattenSeq <*(f . x9)*> by A3, A6
.= <*O*> by A12, PRE_POLY:1 ;
hence S2[nt -tree ts] by A2, A3, A8, Def11; ::_thesis: verum
end;
thus for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch_7(A4, A5); ::_thesis: verum
end;
theorem :: DTCONSTR:14
for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}
proof
let nt be Symbol of PeanoNat; ::_thesis: TerminalLanguage nt = {<*0*>}
A1: ( nt = S or nt = O ) by Lm2, TARSKI:def_2;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= TerminalLanguage nt
let x be set ; ::_thesis: ( x in TerminalLanguage nt implies x in {<*0*>} )
assume x in TerminalLanguage nt ; ::_thesis: x in {<*0*>}
then ex tsg being Element of FinTrees the carrier of PeanoNat st
( x = TerminalString tsg & tsg in TS PeanoNat & tsg . {} = nt ) ;
then x = <*O*> by Th13;
hence x in {<*0*>} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in TerminalLanguage nt )
assume x in {<*0*>} ; ::_thesis: x in TerminalLanguage nt
then A2: x = <*O*> by TARSKI:def_1;
reconsider prtO = root-tree O as Element of TS PeanoNat ;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
reconsider srtO = <*prtO*> as FinSequence of TS PeanoNat ;
A3: rtO . {} = O by TREES_4:3;
then S ==> roots <*rtO*> by Lm5, Th4;
then A4: S -tree <*prtO*> in TS PeanoNat by Def1;
then A5: TerminalString (S -tree srtO) = x by A2, Th13;
A6: (S -tree <*rtO*>) . {} = S by TREES_4:def_4;
TerminalString rtO = x by A2, Th13;
hence x in TerminalLanguage nt by A1, A3, A4, A5, A6; ::_thesis: verum
end;
theorem Th15: :: DTCONSTR:15
for t being Element of TS PeanoNat holds PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
proof
consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that
A1: PreTraversal (root-tree O) = f . (root-tree O) and
A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = <*t*> and
A3: for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) by Def12;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means ex t being Element of TS PeanoNat st
( $1 = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> );
A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_
S2[_root-tree_s]
let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] )
assume A5: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s]
thus S2[ root-tree s] ::_thesis: verum
proof
take t = rtO; ::_thesis: ( root-tree s = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> )
thus root-tree s = t by A5, Lm10, TARSKI:def_1; ::_thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
thus PreTraversal t = <*O*> by A1, A2
.= {} ^ <*O*> by FINSEQ_1:34
.= (0 |-> 1) ^ <*0*>
.= ((height (dom t)) |-> 1) ^ <*0*> by TREES_1:42, TREES_4:3 ; ::_thesis: verum
end;
end;
A6: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat
for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_
S2[t]_)_holds_
S2[nt_-tree_ts]
let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; ::_thesis: S2[nt -tree ts]
reconsider t9 = nt -tree ts as Element of TS PeanoNat by A7, Def1;
A9: nt = S by A7, Def2;
( roots ts = <*O*> or roots ts = <*1*> ) by A7, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A10: ts = <*x*> and
A11: x in TS PeanoNat by Th5;
reconsider x9 = x as Element of TS PeanoNat by A11;
rng ts = {x} by A10, FINSEQ_1:39;
then x in rng ts by TARSKI:def_1;
then A12: ex t9 being Element of TS PeanoNat st
( x = t9 & PreTraversal t9 = ((height (dom t9)) |-> 1) ^ <*0*> ) by A8;
f . x9 is Element of the carrier of PeanoNat * ;
then A13: f . x9 = ((height (dom x9)) |-> 1) ^ <*0*> by A2, A3, A12, Def12;
f * ts = <*(f . x)*> by A10, FINSEQ_2:35;
then A14: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq <*(f . x9)*>) by A3, A7
.= <*nt*> ^ (((height (dom x9)) |-> 1) ^ <*0*>) by A13, PRE_POLY:1
.= (<*nt*> ^ ((height (dom x9)) |-> 1)) ^ <*0*> by FINSEQ_1:32
.= ((1 |-> 1) ^ ((height (dom x9)) |-> 1)) ^ <*0*> by A9, FINSEQ_2:59
.= (((height (dom x9)) + 1) |-> 1) ^ <*0*> by FINSEQ_2:123
.= ((height (^ (dom x9))) |-> 1) ^ <*0*> by TREES_3:80 ;
A15: dom (nt -tree x9) = ^ (dom x9) by TREES_4:13;
A16: t9 = nt -tree x9 by A10, TREES_4:def_5;
f . t9 is Element of the carrier of PeanoNat * ;
then PreTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def12;
hence S2[nt -tree ts] by A14, A15, A16; ::_thesis: verum
end;
A17: for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch_7(A4, A6);
let t be Element of TS PeanoNat; ::_thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*>
S2[t] by A17;
hence PreTraversal t = ((height (dom t)) |-> 1) ^ <*0*> ; ::_thesis: verum
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
let nt be Symbol of PeanoNat; ::_thesis: ( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) )
reconsider rtO = root-tree O as Element of TS PeanoNat ;
height (dom (root-tree 0)) = 0 by TREES_1:42, TREES_4:3;
then PreTraversal rtO = (0 |-> 1) ^ <*O*> by Th15;
then A1: PreTraversal rtO = {} ^ <*O*>
.= <*O*> by FINSEQ_1:34 ;
thus ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) ::_thesis: ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } )
proof
assume A2: nt = 0 ; ::_thesis: PreTraversalLanguage nt = {<*0*>}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= PreTraversalLanguage nt
let x be set ; ::_thesis: ( x in PreTraversalLanguage nt implies x in {<*0*>} )
assume x in PreTraversalLanguage nt ; ::_thesis: x in {<*0*>}
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A3: x = PreTraversal tsg and
A4: tsg in TS PeanoNat and
A5: tsg . {} = O by A2;
tsg = root-tree O by A4, A5, Th9;
hence x in {<*0*>} by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in PreTraversalLanguage nt )
assume x in {<*0*>} ; ::_thesis: x in PreTraversalLanguage nt
then A6: x = <*O*> by TARSKI:def_1;
rtO . {} = O by TREES_4:3;
hence x in PreTraversalLanguage nt by A1, A2, A6; ::_thesis: verum
end;
assume A7: nt = 1 ; ::_thesis: PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } c= PreTraversalLanguage nt
let x be set ; ::_thesis: ( x in PreTraversalLanguage nt implies x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } )
assume x in PreTraversalLanguage nt ; ::_thesis: x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 }
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A8: x = PreTraversal tsg and
A9: tsg in TS PeanoNat and
A10: tsg . {} = S by A7;
consider ts being FinSequence of TS PeanoNat such that
A11: tsg = S -tree ts and
A12: S ==> roots ts by A9, A10, Th10;
( roots ts = <*0*> or roots ts = <*1*> ) by A12, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider t being Element of FinTrees the carrier of PeanoNat such that
A13: ts = <*t*> and
t in TS PeanoNat by Th5;
tsg = S -tree t by A11, A13, TREES_4:def_5;
then dom tsg = ^ (dom t) by TREES_4:13;
then A14: height (dom tsg) = (height (dom t)) + 1 by TREES_3:80;
x = ((height (dom tsg)) |-> 1) ^ <*0*> by A8, A9, Th15;
hence x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } by A14; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } or x in PreTraversalLanguage nt )
assume x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ; ::_thesis: x in PreTraversalLanguage nt
then consider n being Element of NAT such that
A15: x = (n |-> 1) ^ <*0*> and
A16: n <> 0 ;
defpred S2[ Element of NAT ] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ($1 |-> 1) ^ <*0*> ) );
A17: S2[ 0 ] ;
A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A19: S2[n] ; ::_thesis: S2[n + 1]
thus S2[n + 1] ::_thesis: verum
proof
assume n + 1 <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )
then consider tsg being Element of TS PeanoNat such that
tsg . {} = S and
A20: PreTraversal tsg = (n |-> 1) ^ <*0*> by A19;
PreTraversal tsg = ((height (dom tsg)) |-> 1) ^ <*0*> by Th15;
then A21: n |-> 1 = (height (dom tsg)) |-> 1 by A20, FINSEQ_1:33;
len (n |-> 1) = n by CARD_1:def_7;
then A22: height (dom tsg) = n by A21, CARD_1:def_7;
take tsg9 = S -tree tsg; ::_thesis: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> )
A23: tsg9 = S -tree <*tsg*> by TREES_4:def_5;
height (dom tsg9) = height (^ (dom tsg)) by TREES_4:13
.= n + 1 by A22, TREES_3:80 ;
hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A23, Th15, TREES_4:def_4; ::_thesis: verum
end;
supposeA24: n = 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )
take tsg9 = S -tree rtO; ::_thesis: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> )
A25: tsg9 = S -tree <*rtO*> by TREES_4:def_5;
height (dom tsg9) = height (^ (dom rtO)) by TREES_4:13
.= (height (dom rtO)) + 1 by TREES_3:80
.= n + 1 by A24, TREES_1:42, TREES_4:3 ;
hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A25, Th15, TREES_4:def_4; ::_thesis: verum
end;
end;
end;
end;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A17, A18);
then ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = (n |-> 1) ^ <*0*> ) by A16;
hence x in PreTraversalLanguage nt by A7, A15; ::_thesis: verum
end;
theorem Th17: :: DTCONSTR:17
for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
proof
consider f being Function of (TS PeanoNat),( the carrier of PeanoNat *) such that
A1: PostTraversal (root-tree O) = f . (root-tree O) and
A2: for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = <*t*> and
A3: for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> by Def13;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
defpred S2[ DecoratedTree of the carrier of PeanoNat] means ex t being Element of TS PeanoNat st
( $1 = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) );
A4: now__::_thesis:_for_s_being_Symbol_of_PeanoNat_st_s_in_Terminals_PeanoNat_holds_
S2[_root-tree_s]
let s be Symbol of PeanoNat; ::_thesis: ( s in Terminals PeanoNat implies S2[ root-tree s] )
assume A5: s in Terminals PeanoNat ; ::_thesis: S2[ root-tree s]
thus S2[ root-tree s] ::_thesis: verum
proof
take t = rtO; ::_thesis: ( root-tree s = t & PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) )
thus root-tree s = t by A5, Lm10, TARSKI:def_1; ::_thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
thus PostTraversal t = <*O*> by A1, A2
.= <*O*> ^ {} by FINSEQ_1:34
.= <*0*> ^ (0 |-> 1)
.= <*0*> ^ ((height (dom t)) |-> 1) by TREES_1:42, TREES_4:3 ; ::_thesis: verum
end;
end;
A6: now__::_thesis:_for_nt_being_Symbol_of_PeanoNat
for_ts_being_FinSequence_of_TS_PeanoNat_st_nt_==>_roots_ts_&_(_for_t_being_DecoratedTree_of_the_carrier_of_PeanoNat_st_t_in_rng_ts_holds_
S2[t]_)_holds_
S2[nt_-tree_ts]
let nt be Symbol of PeanoNat; ::_thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS PeanoNat; ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S2[t] ; ::_thesis: S2[nt -tree ts]
reconsider t9 = nt -tree ts as Element of TS PeanoNat by A7, Def1;
A9: nt = S by A7, Def2;
( roots ts = <*O*> or roots ts = <*1*> ) by A7, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A10: ts = <*x*> and
A11: x in TS PeanoNat by Th5;
reconsider x9 = x as Element of TS PeanoNat by A11;
rng ts = {x} by A10, FINSEQ_1:39;
then x in rng ts by TARSKI:def_1;
then A12: ex t9 being Element of TS PeanoNat st
( x = t9 & PostTraversal t9 = <*O*> ^ ((height (dom t9)) |-> 1) ) by A8;
f . x9 is Element of the carrier of PeanoNat * ;
then A13: f . x9 = <*O*> ^ ((height (dom x9)) |-> 1) by A2, A3, A12, Def13;
f * ts = <*(f . x)*> by A10, FINSEQ_2:35;
then A14: f . (nt -tree ts) = (FlattenSeq <*(f . x9)*>) ^ <*nt*> by A3, A7
.= (<*O*> ^ ((height (dom x9)) |-> 1)) ^ <*nt*> by A13, PRE_POLY:1
.= <*O*> ^ (((height (dom x9)) |-> 1) ^ <*nt*>) by FINSEQ_1:32
.= <*O*> ^ (((height (dom x9)) |-> 1) ^ (1 |-> 1)) by A9, FINSEQ_2:59
.= <*O*> ^ (((height (dom x9)) + 1) |-> 1) by FINSEQ_2:123
.= <*O*> ^ ((height (^ (dom x9))) |-> 1) by TREES_3:80 ;
A15: dom (nt -tree x9) = ^ (dom x9) by TREES_4:13;
A16: t9 = nt -tree x9 by A10, TREES_4:def_5;
f . t9 is Element of the carrier of PeanoNat * ;
then PostTraversal (nt -tree ts) = f . (nt -tree ts) by A2, A3, Def13;
hence S2[nt -tree ts] by A14, A15, A16; ::_thesis: verum
end;
A17: for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S2[t] from DTCONSTR:sch_7(A4, A6);
let t be Element of TS PeanoNat; ::_thesis: PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)
S2[t] by A17;
hence PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1) ; ::_thesis: verum
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
let nt be Symbol of PeanoNat; ::_thesis: ( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) )
reconsider rtO = root-tree O as Element of TS PeanoNat ;
height (dom (root-tree 0)) = 0 by TREES_1:42, TREES_4:3;
then PostTraversal rtO = <*0*> ^ (0 |-> 1) by Th17;
then A1: PostTraversal rtO = <*O*> ^ {}
.= <*O*> by FINSEQ_1:34 ;
thus ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) ::_thesis: ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )
proof
assume A2: nt = 0 ; ::_thesis: PostTraversalLanguage nt = {<*0*>}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {<*0*>} c= PostTraversalLanguage nt
let x be set ; ::_thesis: ( x in PostTraversalLanguage nt implies x in {<*0*>} )
assume x in PostTraversalLanguage nt ; ::_thesis: x in {<*0*>}
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A3: x = PostTraversal tsg and
A4: tsg in TS PeanoNat and
A5: tsg . {} = O by A2;
tsg = root-tree O by A4, A5, Th9;
hence x in {<*0*>} by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*0*>} or x in PostTraversalLanguage nt )
assume x in {<*0*>} ; ::_thesis: x in PostTraversalLanguage nt
then A6: x = <*O*> by TARSKI:def_1;
rtO . {} = O by TREES_4:3;
hence x in PostTraversalLanguage nt by A1, A2, A6; ::_thesis: verum
end;
assume A7: nt = 1 ; ::_thesis: PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } c= PostTraversalLanguage nt
let x be set ; ::_thesis: ( x in PostTraversalLanguage nt implies x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )
assume x in PostTraversalLanguage nt ; ::_thesis: x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 }
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A8: x = PostTraversal tsg and
A9: tsg in TS PeanoNat and
A10: tsg . {} = S by A7;
consider ts being FinSequence of TS PeanoNat such that
A11: tsg = S -tree ts and
A12: S ==> roots ts by A9, A10, Th10;
( roots ts = <*0*> or roots ts = <*1*> ) by A12, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider t being Element of FinTrees the carrier of PeanoNat such that
A13: ts = <*t*> and
t in TS PeanoNat by Th5;
tsg = S -tree t by A11, A13, TREES_4:def_5;
then dom tsg = ^ (dom t) by TREES_4:13;
then A14: height (dom tsg) = (height (dom t)) + 1 by TREES_3:80;
x = <*0*> ^ ((height (dom tsg)) |-> 1) by A8, A9, Th17;
hence x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } by A14; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } or x in PostTraversalLanguage nt )
assume x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ; ::_thesis: x in PostTraversalLanguage nt
then consider n being Element of NAT such that
A15: x = <*0*> ^ (n |-> 1) and
A16: n <> 0 ;
defpred S2[ Element of NAT ] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ ($1 |-> 1) ) );
A17: S2[ 0 ] ;
A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A19: S2[n] ; ::_thesis: S2[n + 1]
thus S2[n + 1] ::_thesis: verum
proof
assume n + 1 <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) )
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) )
then consider tsg being Element of TS PeanoNat such that
tsg . {} = S and
A20: PostTraversal tsg = <*0*> ^ (n |-> 1) by A19;
PostTraversal tsg = <*0*> ^ ((height (dom tsg)) |-> 1) by Th17;
then A21: n |-> 1 = (height (dom tsg)) |-> 1 by A20, FINSEQ_1:33;
len (n |-> 1) = n by CARD_1:def_7;
then A22: height (dom tsg) = n by A21, CARD_1:def_7;
take tsg9 = S -tree tsg; ::_thesis: ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) )
A23: tsg9 = S -tree <*tsg*> by TREES_4:def_5;
height (dom tsg9) = height (^ (dom tsg)) by TREES_4:13
.= n + 1 by A22, TREES_3:80 ;
hence ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A23, Th17, TREES_4:def_4; ::_thesis: verum
end;
supposeA24: n = 0 ; ::_thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) )
take tsg9 = S -tree rtO; ::_thesis: ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) )
A25: tsg9 = S -tree <*rtO*> by TREES_4:def_5;
height (dom tsg9) = height (^ (dom rtO)) by TREES_4:13
.= (height (dom rtO)) + 1 by TREES_3:80
.= n + 1 by A24, TREES_1:42, TREES_4:3 ;
hence ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A25, Th17, TREES_4:def_4; ::_thesis: verum
end;
end;
end;
end;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A17, A18);
then ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ (n |-> 1) ) by A16;
hence x in PostTraversalLanguage nt by A7, A15; ::_thesis: verum
end;