:: TREES_9 semantic presentation
begin
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;
registration
cluster non empty finite Tree-like -> finite-order for set ;
coherence
for b1 being Tree st b1 is finite holds
b1 is finite-order
proof
let t be Tree; ::_thesis: ( t is finite implies t is finite-order )
assume t is finite ; ::_thesis: t is finite-order
then reconsider s = t as finite Tree ;
take n = (card s) + 1; :: according to TREES_2:def_2 ::_thesis: for b1 being Element of t holds not b1 ^ <*n*> in t
let x be Element of t; ::_thesis: not x ^ <*n*> in t
deffunc H1( Nat) -> set = x ^ <*(c1 - 1)*>;
consider f being FinSequence such that
A1: ( len f = n & ( for i being Nat st i in dom f holds
f . i = H1(i) ) ) from FINSEQ_1:sch_2();
A2: dom f = Seg n by A1, FINSEQ_1:def_3;
assume A3: x ^ <*n*> in t ; ::_thesis: contradiction
A4: rng f c= succ x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in succ x )
assume y in rng f ; ::_thesis: y in succ x
then consider i being set such that
A5: i in dom f and
A6: y = f . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A5;
i >= 1 by A2, A5, FINSEQ_1:1;
then consider j being Nat such that
A7: i = 1 + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A8: j <= i by A7, NAT_1:11;
i <= n by A2, A5, FINSEQ_1:1;
then j <= n by A8, XXREAL_0:2;
then A9: x ^ <*j*> in t by A3, TREES_1:def_3;
i - 1 = j by A7;
then y = x ^ <*j*> by A1, A5, A6;
hence y in succ x by A9; ::_thesis: verum
end;
A10: card (succ x) c= card t by CARD_1:11;
f is one-to-one
proof
let z, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z in proj1 f or not y in proj1 f or not f . z = f . y or z = y )
assume that
A11: ( z in dom f & y in dom f ) and
A12: f . z = f . y ; ::_thesis: z = y
reconsider i1 = z, i2 = y as Element of NAT by A11;
( f . z = x ^ <*(i1 - 1)*> & f . y = x ^ <*(i2 - 1)*> ) by A1, A11;
then <*(i1 - 1)*> = <*(i2 - 1)*> by A12, FINSEQ_1:33;
then i1 - 1 = <*(i2 - 1)*> . 1 by FINSEQ_1:40
.= i2 - 1 by FINSEQ_1:40 ;
hence z = y ; ::_thesis: verum
end;
then card (dom f) c= card (succ x) by A4, CARD_1:10;
then A13: card (dom f) c= card t by A10, XBOOLE_1:1;
A14: card s <= n by NAT_1:11;
card (Seg n) = n by FINSEQ_1:57;
then n <= card s by A2, A13, NAT_1:39;
then n = (card s) + 0 by A14, XXREAL_0:1;
hence contradiction ; ::_thesis: verum
end;
end;
Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
proof
let n be set ; ::_thesis: for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
let p be FinSequence; ::_thesis: ( n in dom p implies ex k being Element of NAT st
( n = k + 1 & k < len p ) )
assume A1: n in dom p ; ::_thesis: ex k being Element of NAT st
( n = k + 1 & k < len p )
then reconsider n = n as Element of NAT ;
n >= 1 by A1, FINSEQ_3:25;
then consider k being Nat such that
A2: n = 1 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: ( n = k + 1 & k < len p )
n <= len p by A1, FINSEQ_3:25;
hence ( n = k + 1 & k < len p ) by A2, NAT_1:13; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_p,_q_being_FinSequence_st_len_p_=_len_q_&_(_for_i_being_Element_of_NAT_st_i_<_len_p_holds_
p_._(i_+_1)_=_q_._(i_+_1)_)_holds_
p_=_q
let p, q be FinSequence; ::_thesis: ( len p = len q & ( for i being Element of NAT st i < len p holds
p . (i + 1) = q . (i + 1) ) implies p = q )
assume that
A1: len p = len q and
A2: for i being Element of NAT st i < len p holds
p . (i + 1) = q . (i + 1) ; ::_thesis: p = q
A3: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
p_._i_=_q_._i
let i be Nat; ::_thesis: ( i in dom p implies p . i = q . i )
assume i in dom p ; ::_thesis: p . i = q . i
then ex k being Element of NAT st
( i = k + 1 & k < len p ) by Lm1;
hence p . i = q . i by A2; ::_thesis: verum
end;
dom p = dom q by A1, FINSEQ_3:29;
hence p = q by A3, FINSEQ_1:13; ::_thesis: verum
end;
Lm3: for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
proof
let n be Element of NAT ; ::_thesis: for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let p be FinSequence; ::_thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
n >= 0 by NAT_1:2;
then A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; ::_thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
then n + 1 <= len p by NAT_1:13;
then n + 1 in dom p by A1, FINSEQ_3:25;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def_3; ::_thesis: verum
end;
Lm4: now__::_thesis:_for_p_being_FinSequence
for_x_being_set_st_x_in_rng_p_holds_
ex_k_being_Element_of_NAT_st_
(_k_<_len_p_&_x_=_p_._(k_+_1)_)
let p be FinSequence; ::_thesis: for x being set st x in rng p holds
ex k being Element of NAT st
( k < len p & x = p . (k + 1) )
let x be set ; ::_thesis: ( x in rng p implies ex k being Element of NAT st
( k < len p & x = p . (k + 1) ) )
assume x in rng p ; ::_thesis: ex k being Element of NAT st
( k < len p & x = p . (k + 1) )
then consider y being set such that
A1: y in dom p and
A2: x = p . y by FUNCT_1:def_3;
ex k being Element of NAT st
( y = k + 1 & k < len p ) by A1, Lm1;
hence ex k being Element of NAT st
( k < len p & x = p . (k + 1) ) by A2; ::_thesis: verum
end;
theorem Th1: :: TREES_9:1
for t being DecoratedTree holds t | (<*> NAT) = t
proof
let t be DecoratedTree; ::_thesis: t | (<*> NAT) = t
A1: dom (t | (<*> NAT)) = (dom t) | (<*> NAT) by TREES_2:def_10;
now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_dom_(t_|_(<*>_NAT))_holds_
(t_|_(<*>_NAT))_._p_=_t_._p
let p be FinSequence of NAT ; ::_thesis: ( p in dom (t | (<*> NAT)) implies (t | (<*> NAT)) . p = t . p )
assume p in dom (t | (<*> NAT)) ; ::_thesis: (t | (<*> NAT)) . p = t . p
hence (t | (<*> NAT)) . p = t . ({} ^ p) by A1, TREES_2:def_10
.= t . p by FINSEQ_1:34 ;
::_thesis: verum
end;
hence t | (<*> NAT) = t by A1, TREES_1:31, TREES_2:31; ::_thesis: verum
end;
theorem Th2: :: TREES_9:2
for t being Tree
for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q
proof
let t be Tree; ::_thesis: for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q
let p, q be FinSequence of NAT ; ::_thesis: ( p ^ q in t implies t | (p ^ q) = (t | p) | q )
assume A1: p ^ q in t ; ::_thesis: t | (p ^ q) = (t | p) | q
let r be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) )
A2: p in t by A1, TREES_1:21;
then q in t | p by A1, TREES_1:def_6;
then A3: ( r in (t | p) | q iff q ^ r in t | p ) by TREES_1:def_6;
A4: (p ^ q) ^ r = p ^ (q ^ r) by FINSEQ_1:32;
( r in t | (p ^ q) iff (p ^ q) ^ r in t ) by A1, TREES_1:def_6;
hence ( ( not r in t | (p ^ q) or r in (t | p) | q ) & ( not r in (t | p) | q or r in t | (p ^ q) ) ) by A2, A4, A3, TREES_1:def_6; ::_thesis: verum
end;
theorem Th3: :: TREES_9:3
for t being DecoratedTree
for p, q being FinSequence of NAT st p ^ q in dom t holds
t | (p ^ q) = (t | p) | q
proof
let t be DecoratedTree; ::_thesis: for p, q being FinSequence of NAT st p ^ q in dom t holds
t | (p ^ q) = (t | p) | q
let p, q be FinSequence of NAT ; ::_thesis: ( p ^ q in dom t implies t | (p ^ q) = (t | p) | q )
A1: dom (t | p) = (dom t) | p by TREES_2:def_10;
A2: dom (t | (p ^ q)) = (dom t) | (p ^ q) by TREES_2:def_10;
assume A3: p ^ q in dom t ; ::_thesis: t | (p ^ q) = (t | p) | q
then A4: p in dom t by TREES_1:21;
then A5: q in (dom t) | p by A3, TREES_1:def_6;
A6: now__::_thesis:_for_a_being_FinSequence_of_NAT_st_a_in_dom_(t_|_(p_^_q))_holds_
(t_|_(p_^_q))_._a_=_((t_|_p)_|_q)_._a
let a be FinSequence of NAT ; ::_thesis: ( a in dom (t | (p ^ q)) implies (t | (p ^ q)) . a = ((t | p) | q) . a )
A7: (p ^ q) ^ a = p ^ (q ^ a) by FINSEQ_1:32;
assume A8: a in dom (t | (p ^ q)) ; ::_thesis: (t | (p ^ q)) . a = ((t | p) | q) . a
then (p ^ q) ^ a in dom t by A3, A2, TREES_1:def_6;
then A9: q ^ a in (dom t) | p by A4, A7, TREES_1:def_6;
then A10: a in ((dom t) | p) | q by A5, TREES_1:def_6;
thus (t | (p ^ q)) . a = t . ((p ^ q) ^ a) by A2, A8, TREES_2:def_10
.= (t | p) . (q ^ a) by A7, A9, TREES_2:def_10
.= ((t | p) | q) . a by A1, A10, TREES_2:def_10 ; ::_thesis: verum
end;
dom ((t | p) | q) = (dom (t | p)) | q by TREES_2:def_10;
hence t | (p ^ q) = (t | p) | q by A3, A1, A2, A6, Th2, TREES_2:31; ::_thesis: verum
end;
notation
let IT be DecoratedTree;
synonym root IT for trivial ;
end;
definition
let IT be DecoratedTree;
redefine attr IT is trivial means :Def1: :: TREES_9:def 1
dom IT = elementary_tree 0;
compatibility
( IT is root iff dom IT = elementary_tree 0 )
proof
thus ( IT is root implies dom IT = elementary_tree 0 ) ::_thesis: ( dom IT = elementary_tree 0 implies IT is root )
proof
not dom IT is empty ;
then A1: not IT is empty ;
assume IT is root ; ::_thesis: dom IT = elementary_tree 0
then consider x being set such that
A2: IT = {x} by A1, ZFMISC_1:131;
x in IT by A2, TARSKI:def_1;
then consider x1, x2 being set such that
A3: x = [x1,x2] by RELAT_1:def_1;
( {} in dom IT & dom IT = {x1} ) by A2, A3, RELAT_1:9, TREES_1:22;
hence dom IT = elementary_tree 0 by TARSKI:def_1, TREES_1:29; ::_thesis: verum
end;
thus ( dom IT = elementary_tree 0 implies IT is root ) by TREES_1:29; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines root TREES_9:def_1_:_
for IT being DecoratedTree holds
( IT is root iff dom IT = elementary_tree 0 );
theorem Th4: :: TREES_9:4
for t being DecoratedTree holds
( t is root iff {} in Leaves (dom t) )
proof
let t be DecoratedTree; ::_thesis: ( t is root iff {} in Leaves (dom t) )
reconsider e = {} as Node of t by TREES_1:22;
hereby ::_thesis: ( {} in Leaves (dom t) implies t is root )
assume t is root ; ::_thesis: {} in Leaves (dom t)
then dom t = elementary_tree 0 by Def1;
then not e ^ <*0*> in dom t by TARSKI:def_1, TREES_1:29;
hence {} in Leaves (dom t) by TREES_1:54; ::_thesis: verum
end;
assume A1: {} in Leaves (dom t) ; ::_thesis: t is root
let p be FinSequence of NAT ; :: according to TREES_2:def_1,TREES_9:def_1 ::_thesis: ( ( not p in dom t or p in elementary_tree 0 ) & ( not p in elementary_tree 0 or p in dom t ) )
hereby ::_thesis: ( not p in elementary_tree 0 or p in dom t )
assume that
A2: p in dom t and
A3: not p in elementary_tree 0 ; ::_thesis: contradiction
p <> {} by A3, TARSKI:def_1, TREES_1:29;
then consider q being FinSequence of NAT , n being Element of NAT such that
A4: p = <*n*> ^ q by FINSEQ_2:130;
A5: e ^ <*n*> = <*n*> by FINSEQ_1:34;
<*n*> in dom t by A2, A4, TREES_1:21;
hence contradiction by A1, A5, TREES_1:55; ::_thesis: verum
end;
assume p in elementary_tree 0 ; ::_thesis: p in dom t
then p = {} by TARSKI:def_1, TREES_1:29;
hence p in dom t by TREES_1:22; ::_thesis: verum
end;
theorem Th5: :: TREES_9:5
for t being Tree
for p being Element of t holds
( t | p = elementary_tree 0 iff p in Leaves t )
proof
let t be Tree; ::_thesis: for p being Element of t holds
( t | p = elementary_tree 0 iff p in Leaves t )
let p be Element of t; ::_thesis: ( t | p = elementary_tree 0 iff p in Leaves t )
A1: not <*0*> in elementary_tree 0 by TARSKI:def_1, TREES_1:29;
hereby ::_thesis: ( p in Leaves t implies t | p = elementary_tree 0 )
assume t | p = elementary_tree 0 ; ::_thesis: p in Leaves t
then not p ^ <*0*> in t by A1, TREES_1:def_6;
hence p in Leaves t by TREES_1:54; ::_thesis: verum
end;
assume A2: p in Leaves t ; ::_thesis: t | p = elementary_tree 0
let q be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not q in t | p or q in elementary_tree 0 ) & ( not q in elementary_tree 0 or q in t | p ) )
hereby ::_thesis: ( not q in elementary_tree 0 or q in t | p )
assume q in t | p ; ::_thesis: q in elementary_tree 0
then p ^ q in t by TREES_1:def_6;
then A3: not p is_a_proper_prefix_of p ^ q by A2, TREES_1:def_5;
p is_a_prefix_of p ^ q by TREES_1:1;
then p ^ q = p by A3, XBOOLE_0:def_8
.= p ^ {} by FINSEQ_1:34 ;
then q = {} by FINSEQ_1:33;
hence q in elementary_tree 0 by TREES_1:22; ::_thesis: verum
end;
assume q in elementary_tree 0 ; ::_thesis: q in t | p
then q = {} by TARSKI:def_1, TREES_1:29;
hence q in t | p by TREES_1:22; ::_thesis: verum
end;
theorem :: TREES_9:6
for t being DecoratedTree
for p being Node of t holds
( t | p is root iff p in Leaves (dom t) )
proof
let t be DecoratedTree; ::_thesis: for p being Node of t holds
( t | p is root iff p in Leaves (dom t) )
let p be Node of t; ::_thesis: ( t | p is root iff p in Leaves (dom t) )
A1: dom (t | p) = (dom t) | p by TREES_2:def_10;
( t | p is root iff dom (t | p) = elementary_tree 0 ) by Def1;
hence ( t | p is root iff p in Leaves (dom t) ) by A1, Th5; ::_thesis: verum
end;
registration
cluster Relation-like root Function-like DecoratedTree-like for set ;
existence
ex b1 being DecoratedTree st b1 is root
proof
take t = root-tree 0; ::_thesis: t is root
thus dom t = elementary_tree 0 by TREES_4:3; :: according to TREES_9:def_1 ::_thesis: verum
end;
cluster Relation-like non root Function-like finite DecoratedTree-like for set ;
existence
ex b1 being DecoratedTree st
( b1 is finite & not b1 is root )
proof
take t = 0 -tree (root-tree 0); ::_thesis: ( t is finite & not t is root )
dom t = ^ (dom (root-tree 0)) by TREES_4:13
.= elementary_tree 1 by TREES_3:67, TREES_4:3 ;
hence t is finite by FINSET_1:10; ::_thesis: not t is root
assume dom t = elementary_tree 0 ; :: according to TREES_9:def_1 ::_thesis: contradiction
then root-tree (t . {}) = t by TREES_4:5
.= 0 -tree <*(root-tree 0)*> ;
hence contradiction by TREES_4:17; ::_thesis: verum
end;
end;
registration
let x be set ;
cluster root-tree x -> root finite ;
coherence
( root-tree x is finite & root-tree x is root )
proof
dom (root-tree x) = elementary_tree 0 by TREES_4:3;
hence ( root-tree x is finite & root-tree x is root ) by Def1; ::_thesis: verum
end;
end;
definition
let IT be Tree;
attrIT is finite-branching means :Def2: :: TREES_9:def 2
for x being Element of IT holds succ x is finite ;
end;
:: deftheorem Def2 defines finite-branching TREES_9:def_2_:_
for IT being Tree holds
( IT is finite-branching iff for x being Element of IT holds succ x is finite );
registration
cluster non empty Tree-like finite-order -> finite-branching for set ;
coherence
for b1 being Tree st b1 is finite-order holds
b1 is finite-branching
proof
let t be Tree; ::_thesis: ( t is finite-order implies t is finite-branching )
assume t is finite-order ; ::_thesis: t is finite-branching
then reconsider a = t as finite-order Tree ;
let x be Element of t; :: according to TREES_9:def_2 ::_thesis: succ x is finite
reconsider x = x as Element of a ;
succ x is finite ;
hence succ x is finite ; ::_thesis: verum
end;
end;
definition
let IT be DecoratedTree;
attrIT is finite-order means :Def3: :: TREES_9:def 3
dom IT is finite-order ;
attrIT is finite-branching means :Def4: :: TREES_9:def 4
dom IT is finite-branching ;
end;
:: deftheorem Def3 defines finite-order TREES_9:def_3_:_
for IT being DecoratedTree holds
( IT is finite-order iff dom IT is finite-order );
:: deftheorem Def4 defines finite-branching TREES_9:def_4_:_
for IT being DecoratedTree holds
( IT is finite-branching iff dom IT is finite-branching );
registration
cluster Relation-like Function-like finite DecoratedTree-like -> finite-order for set ;
coherence
for b1 being DecoratedTree st b1 is finite holds
b1 is finite-order
proof
let t be DecoratedTree; ::_thesis: ( t is finite implies t is finite-order )
assume t is finite ; ::_thesis: t is finite-order
hence dom t is finite-order ; :: according to TREES_9:def_3 ::_thesis: verum
end;
cluster Relation-like Function-like DecoratedTree-like finite-order -> finite-branching for set ;
coherence
for b1 being DecoratedTree st b1 is finite-order holds
b1 is finite-branching
proof
let t be DecoratedTree; ::_thesis: ( t is finite-order implies t is finite-branching )
assume dom t is finite-order ; :: according to TREES_9:def_3 ::_thesis: t is finite-branching
hence dom t is finite-branching ; :: according to TREES_9:def_4 ::_thesis: verum
end;
end;
registration
let t be finite-order DecoratedTree;
cluster proj1 t -> finite-order ;
coherence
dom t is finite-order by Def3;
end;
registration
let t be finite-branching DecoratedTree;
cluster proj1 t -> finite-branching ;
coherence
dom t is finite-branching by Def4;
end;
registration
let t be finite-branching Tree;
let p be Element of t;
cluster succ p -> finite ;
coherence
succ p is finite by Def2;
end;
scheme :: TREES_9:sch 1
FinOrdSet{ F1( set ) -> set , F2() -> finite set } :
for n being Element of NAT holds
( F1(n) in F2() iff n < card F2() )
provided
A1: for x being set st x in F2() holds
ex n being Element of NAT st x = F1(n) and
A2: for i, j being Element of NAT st i < j & F1(j) in F2() holds
F1(i) in F2() and
A3: for i, j being Element of NAT st F1(i) = F1(j) holds
i = j
proof
consider f being Function such that
A4: ( dom f = card F2() & ( for x being set st x in card F2() holds
f . x = F1(x) ) ) from FUNCT_1:sch_3();
defpred S1[ Element of NAT ] means ( $1 < card F2() implies F1($1) in F2() );
A5: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A6: ( n < card F2() implies F1(n) in F2() ) and
A7: n + 1 < card F2() and
A8: not F1((n + 1)) in F2() ; ::_thesis: contradiction
consider f being Function such that
A9: ( dom f = n + 1 & ( for x being set st x in n + 1 holds
f . x = F1(x) ) ) from FUNCT_1:sch_3();
A10: n + 1 = { k where k is Element of NAT : k < n + 1 } by AXIOMS:4;
A11: n <= n + 1 by NAT_1:11;
A12: rng f = F2()
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: F2() c= rng f
let x be set ; ::_thesis: ( x in rng f implies x in F2() )
assume x in rng f ; ::_thesis: x in F2()
then consider y being set such that
A13: y in n + 1 and
A14: x = f . y by A9, FUNCT_1:def_3;
consider k being Element of NAT such that
A15: y = k and
A16: k < n + 1 by A10, A13;
k <= n by A16, NAT_1:13;
then ( k = n or k < n ) by XXREAL_0:1;
then F1(k) in F2() by A2, A6, A7, A11, XXREAL_0:2;
hence x in F2() by A9, A13, A14, A15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() or x in rng f )
assume A17: x in F2() ; ::_thesis: x in rng f
then consider k being Element of NAT such that
A18: x = F1(k) by A1;
now__::_thesis:_not_k_>=_n_+_1
assume k >= n + 1 ; ::_thesis: contradiction
then ( k = n + 1 or k > n + 1 ) by XXREAL_0:1;
hence contradiction by A2, A8, A17, A18; ::_thesis: verum
end;
then A19: k in n + 1 by A10;
then x = f . k by A9, A18;
hence x in rng f by A9, A19, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A20: x1 in dom f and
A21: x2 in dom f and
A22: f . x1 = f . x2 ; ::_thesis: x1 = x2
( ex k being Element of NAT st
( x1 = k & k < n + 1 ) & ex k being Element of NAT st
( x2 = k & k < n + 1 ) ) by A9, A10, A20, A21;
then A23: ( F1(x1) = F1(x2) implies x1 = x2 ) by A3;
F1(x1) = f . x1 by A9, A20;
hence x1 = x2 by A9, A21, A22, A23; ::_thesis: verum
end;
then n + 1,F2() are_equipotent by A9, A12, WELLORD2:def_4;
hence contradiction by A7, CARD_1:def_2; ::_thesis: verum
end;
A24: card F2() = { n where n is Element of NAT : n < card F2() } by AXIOMS:4;
f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A25: x1 in dom f and
A26: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
( ex k being Element of NAT st
( x1 = k & k < card F2() ) & ex k being Element of NAT st
( x2 = k & k < card F2() ) ) by A4, A24, A25, A26;
then A27: ( F1(x1) = F1(x2) implies x1 = x2 ) by A3;
F1(x1) = f . x1 by A4, A25;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A4, A26, A27; ::_thesis: verum
end;
then A28: dom f, rng f are_equipotent by WELLORD2:def_4;
then reconsider Y = rng f as finite set by A4, CARD_1:38;
A29: card (rng f) = card (card F2()) by A4, A28, CARD_1:5
.= card F2() ;
A30: now__::_thesis:_for_i_being_Element_of_NAT_holds_
(_not_i_>=_card_F2()_or_not_F1(i)_in_F2()_)
given i being Element of NAT such that A31: i >= card F2() and
A32: F1(i) in F2() ; ::_thesis: contradiction
( card F2() < i or card F2() = i ) by A31, XXREAL_0:1;
then A33: F1((card F2())) in F2() by A2, A32;
rng f c= F2() \ {F1((card F2()))}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() \ {F1((card F2()))} )
assume x in rng f ; ::_thesis: x in F2() \ {F1((card F2()))}
then consider y being set such that
A34: y in card F2() and
A35: x = f . y by A4, FUNCT_1:def_3;
consider k being Element of NAT such that
A36: y = k and
A37: k < card F2() by A24, A34;
A38: F1(k) = x by A4, A34, A35, A36;
A39: now__::_thesis:_not_x_in_{F1((card_F2()))}
assume x in {F1((card F2()))} ; ::_thesis: contradiction
then F1(k) = F1((card F2())) by A38, TARSKI:def_1;
hence contradiction by A3, A37; ::_thesis: verum
end;
F1(k) in F2() by A2, A33, A37;
hence x in F2() \ {F1((card F2()))} by A38, A39, XBOOLE_0:def_5; ::_thesis: verum
end;
then A40: card Y <= card (F2() \ {F1((card F2()))}) by NAT_1:43;
{F1((card F2()))} c= F2() by A33, ZFMISC_1:31;
then card Y <= (card F2()) - (card {F1((card F2()))}) by A40, CARD_2:44;
then card Y <= (card Y) - 1 by A29, CARD_2:42;
then (card Y) + 1 <= ((card Y) - 1) + 1 by XREAL_1:7;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
A41: S1[ 0 ]
proof
assume 0 < card F2() ; ::_thesis: F1(0) in F2()
then reconsider X = F2() as non empty set ;
set x = the Element of X;
consider n being Element of NAT such that
A42: the Element of X = F1(n) by A1;
( n = 0 or n > 0 ) by NAT_1:3;
hence F1(0) in F2() by A2, A42; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A41, A5);
hence for n being Element of NAT holds
( F1(n) in F2() iff n < card F2() ) by A30; ::_thesis: verum
end;
theorem Th7: :: TREES_9:7
for t being finite-branching Tree
for p being Element of t
for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
proof
let t be finite-branching Tree; ::_thesis: for p being Element of t
for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
let p be Element of t; ::_thesis: for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
deffunc H1( Element of NAT ) -> FinSequence of NAT = p ^ <*$1*>;
A1: for x being set st x in succ p holds
ex n being Element of NAT st x = H1(n)
proof
let x be set ; ::_thesis: ( x in succ p implies ex n being Element of NAT st x = H1(n) )
assume x in succ p ; ::_thesis: ex n being Element of NAT st x = H1(n)
then ex n being Element of NAT st
( x = H1(n) & H1(n) in t ) ;
hence ex n being Element of NAT st x = H1(n) ; ::_thesis: verum
end;
A2: for i, j being Element of NAT st i < j & H1(j) in succ p holds
H1(i) in succ p
proof
let i, j be Element of NAT ; ::_thesis: ( i < j & H1(j) in succ p implies H1(i) in succ p )
assume ( i < j & p ^ <*j*> in succ p ) ; ::_thesis: H1(i) in succ p
then p ^ <*i*> in t by TREES_1:def_3;
hence H1(i) in succ p ; ::_thesis: verum
end;
A3: for i, j being Element of NAT st H1(i) = H1(j) holds
i = j
proof
let i, j be Element of NAT ; ::_thesis: ( H1(i) = H1(j) implies i = j )
assume p ^ <*i*> = p ^ <*j*> ; ::_thesis: i = j
hence i = (p ^ <*j*>) . ((len p) + 1) by FINSEQ_1:42
.= j by FINSEQ_1:42 ;
::_thesis: verum
end;
thus for n being Element of NAT holds
( H1(n) in succ p iff n < card (succ p) ) from TREES_9:sch_1(A1, A2, A3); ::_thesis: verum
end;
definition
let t be finite-branching Tree;
let p be Element of t;
funcp succ -> one-to-one FinSequence of t means :Def5: :: TREES_9:def 5
( len it = card (succ p) & rng it = succ p & ( for i being Element of NAT st i < len it holds
it . (i + 1) = p ^ <*i*> ) );
existence
ex b1 being one-to-one FinSequence of t st
( len b1 = card (succ p) & rng b1 = succ p & ( for i being Element of NAT st i < len b1 holds
b1 . (i + 1) = p ^ <*i*> ) )
proof
deffunc H1( Nat) -> set = p ^ <*($1 - 1)*>;
consider q being FinSequence such that
A1: ( len q = card (succ p) & ( for i being Nat st i in dom q holds
q . i = H1(i) ) ) from FINSEQ_1:sch_2();
A2: q is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 q or not x2 in proj1 q or not q . x1 = q . x2 or x1 = x2 )
assume A3: ( x1 in dom q & x2 in dom q ) ; ::_thesis: ( not q . x1 = q . x2 or x1 = x2 )
then reconsider i1 = x1, i2 = x2 as Element of NAT ;
A4: ( (p ^ <*(i1 - 1)*>) . ((len p) + 1) = i1 - 1 & (p ^ <*(i2 - 1)*>) . ((len p) + 1) = i2 - 1 ) by FINSEQ_1:42;
( q . x1 = p ^ <*(i1 - 1)*> & q . x2 = p ^ <*(i2 - 1)*> ) by A1, A3;
hence ( not q . x1 = q . x2 or x1 = x2 ) by A4; ::_thesis: verum
end;
A5: for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*>
proof
let i be Element of NAT ; ::_thesis: ( i < len q implies q . (i + 1) = p ^ <*i*> )
assume i < len q ; ::_thesis: q . (i + 1) = p ^ <*i*>
then q . (i + 1) = p ^ <*((i + 1) - 1)*> by A1, Lm3;
hence q . (i + 1) = p ^ <*i*> ; ::_thesis: verum
end;
A6: rng q c= succ p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in succ p )
assume x in rng q ; ::_thesis: x in succ p
then consider k being Element of NAT such that
A7: k < len q and
A8: x = q . (k + 1) by Lm4;
x = p ^ <*k*> by A5, A7, A8;
hence x in succ p by A1, A7, Th7; ::_thesis: verum
end;
then reconsider q = q as one-to-one FinSequence of succ p by A2, FINSEQ_1:def_4;
take q ; ::_thesis: ( len q = card (succ p) & rng q = succ p & ( for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> ) )
thus ( len q = card (succ p) & rng q c= succ p ) by A1, A6; :: according to XBOOLE_0:def_10 ::_thesis: ( succ p c= rng q & ( for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> ) )
thus succ p c= rng q ::_thesis: for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ p or x in rng q )
assume A9: x in succ p ; ::_thesis: x in rng q
then consider n being Element of NAT such that
A10: x = p ^ <*n*> and
p ^ <*n*> in t ;
A11: n < card (succ p) by A9, A10, Th7;
then q . (n + 1) = x by A1, A5, A10;
hence x in rng q by A1, A11, Lm3; ::_thesis: verum
end;
thus for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> by A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being one-to-one FinSequence of t st len b1 = card (succ p) & rng b1 = succ p & ( for i being Element of NAT st i < len b1 holds
b1 . (i + 1) = p ^ <*i*> ) & len b2 = card (succ p) & rng b2 = succ p & ( for i being Element of NAT st i < len b2 holds
b2 . (i + 1) = p ^ <*i*> ) holds
b1 = b2
proof
let q1, q2 be one-to-one FinSequence of t; ::_thesis: ( len q1 = card (succ p) & rng q1 = succ p & ( for i being Element of NAT st i < len q1 holds
q1 . (i + 1) = p ^ <*i*> ) & len q2 = card (succ p) & rng q2 = succ p & ( for i being Element of NAT st i < len q2 holds
q2 . (i + 1) = p ^ <*i*> ) implies q1 = q2 )
assume that
A12: len q1 = card (succ p) and
rng q1 = succ p and
A13: for i being Element of NAT st i < len q1 holds
q1 . (i + 1) = p ^ <*i*> and
A14: len q2 = card (succ p) and
rng q2 = succ p and
A15: for i being Element of NAT st i < len q2 holds
q2 . (i + 1) = p ^ <*i*> ; ::_thesis: q1 = q2
A16: dom q1 = Seg (card (succ p)) by A12, FINSEQ_1:def_3;
A17: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(card_(succ_p))_holds_
q1_._k_=_q2_._k
let k be Nat; ::_thesis: ( k in Seg (card (succ p)) implies q1 . k = q2 . k )
assume k in Seg (card (succ p)) ; ::_thesis: q1 . k = q2 . k
then consider n being Element of NAT such that
A18: ( k = n + 1 & n < len q1 ) by A16, Lm1;
thus q1 . k = p ^ <*n*> by A13, A18
.= q2 . k by A12, A14, A15, A18 ; ::_thesis: verum
end;
dom q2 = Seg (card (succ p)) by A14, FINSEQ_1:def_3;
hence q1 = q2 by A16, A17, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines succ TREES_9:def_5_:_
for t being finite-branching Tree
for p being Element of t
for b3 being one-to-one FinSequence of t holds
( b3 = p succ iff ( len b3 = card (succ p) & rng b3 = succ p & ( for i being Element of NAT st i < len b3 holds
b3 . (i + 1) = p ^ <*i*> ) ) );
definition
let t be finite-branching DecoratedTree;
let p be FinSequence;
assume A1: p in dom t ;
func succ (t,p) -> FinSequence means :Def6: :: TREES_9:def 6
ex q being Element of dom t st
( q = p & it = t * (q succ) );
existence
ex b1 being FinSequence ex q being Element of dom t st
( q = p & b1 = t * (q succ) )
proof
reconsider q = p as Element of dom t by A1;
rng (q succ) c= dom t ;
then dom (t * (q succ)) = dom (q succ) by RELAT_1:27
.= Seg (len (q succ)) by FINSEQ_1:def_3 ;
then t * (q succ) is FinSequence by FINSEQ_1:def_2;
hence ex b1 being FinSequence ex q being Element of dom t st
( q = p & b1 = t * (q succ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st ex q being Element of dom t st
( q = p & b1 = t * (q succ) ) & ex q being Element of dom t st
( q = p & b2 = t * (q succ) ) holds
b1 = b2 ;
end;
:: deftheorem Def6 defines succ TREES_9:def_6_:_
for t being finite-branching DecoratedTree
for p being FinSequence st p in dom t holds
for b3 being FinSequence holds
( b3 = succ (t,p) iff ex q being Element of dom t st
( q = p & b3 = t * (q succ) ) );
theorem Th8: :: TREES_9:8
for t being finite-branching DecoratedTree ex x being set ex p being DTree-yielding FinSequence st t = x -tree p
proof
let t be finite-branching DecoratedTree; ::_thesis: ex x being set ex p being DTree-yielding FinSequence st t = x -tree p
take t . {} ; ::_thesis: ex p being DTree-yielding FinSequence st t = (t . {}) -tree p
reconsider e = {} as Node of t by TREES_1:22;
defpred S1[ set , set ] means ex n being Element of NAT st
( n + 1 = $1 & $2 = t | <*n*> );
(dom t) -level 1 = succ e by TREES_2:13;
then reconsider A = (dom t) -level 1 as finite set ;
reconsider e = {} as Element of dom t by TREES_1:22;
A1: for z being set st z in Seg (card A) holds
ex u being set st S1[z,u]
proof
let z be set ; ::_thesis: ( z in Seg (card A) implies ex u being set st S1[z,u] )
assume A2: z in Seg (card A) ; ::_thesis: ex u being set st S1[z,u]
then reconsider m = z as Element of NAT ;
m >= 1 by A2, FINSEQ_1:1;
then consider n being Nat such that
A3: m = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider y = t | <*n*> as set ;
take y ; ::_thesis: S1[z,y]
take n ; ::_thesis: ( n + 1 = z & y = t | <*n*> )
thus ( n + 1 = z & y = t | <*n*> ) by A3; ::_thesis: verum
end;
consider p being Function such that
A4: dom p = Seg (card A) and
A5: for z being set st z in Seg (card A) holds
S1[z,p . z] from CLASSES1:sch_1(A1);
reconsider p = p as FinSequence by A4, FINSEQ_1:def_2;
A6: len p = card A by A4, FINSEQ_1:def_3;
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_is_DecoratedTree
let x be set ; ::_thesis: ( x in dom p implies p . x is DecoratedTree )
assume x in dom p ; ::_thesis: p . x is DecoratedTree
then ex n being Element of NAT st
( n + 1 = x & p . x = t | <*n*> ) by A4, A5;
hence p . x is DecoratedTree ; ::_thesis: verum
end;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_e_^_<*n*>_=_<*n*>_&_succ_e_=_A_&_(_<*n*>_in_A_implies_n_<_card_A_)_&_(_n_<_card_A_implies_<*n*>_in_A_)_)
let n be Element of NAT ; ::_thesis: ( e ^ <*n*> = <*n*> & succ e = A & ( <*n*> in A implies n < card A ) & ( n < card A implies <*n*> in A ) )
thus ( e ^ <*n*> = <*n*> & succ e = A ) by FINSEQ_1:34, TREES_2:13; ::_thesis: ( <*n*> in A iff n < card A )
hence ( <*n*> in A iff n < card A ) by Th7; ::_thesis: verum
end;
reconsider p = p as DTree-yielding FinSequence by A7, TREES_3:24;
A9: len (doms p) = len p by TREES_3:38;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_t_&_x_<>_{}_implies_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_n_<_len_(doms_p)_&_q_in_(doms_p)_._(n_+_1)_&_x_=_<*n*>_^_q_)_)_&_(_(_x_=_{}_or_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_n_<_len_(doms_p)_&_q_in_(doms_p)_._(n_+_1)_&_x_=_<*n*>_^_q_)_)_implies_x_in_dom_t_)_)
let x be set ; ::_thesis: ( ( x in dom t & x <> {} implies ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) & ( ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) implies x in dom t ) )
hereby ::_thesis: ( ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) implies x in dom t )
assume that
A10: x in dom t and
A11: x <> {} ; ::_thesis: ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q )
reconsider r = x as Node of t by A10;
consider q being FinSequence of NAT , n being Element of NAT such that
A12: r = <*n*> ^ q by A11, FINSEQ_2:130;
A13: <*n*> in dom t by A12, TREES_1:21;
reconsider q = q as FinSequence ;
take n = n; ::_thesis: ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q )
take q = q; ::_thesis: ( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q )
e ^ <*n*> = <*n*> by A8;
then <*n*> in A by A8, A13;
hence n < len (doms p) by A6, A8, A9; ::_thesis: ( q in (doms p) . (n + 1) & x = <*n*> ^ q )
then ( n + 1 in dom p & ex k being Element of NAT st
( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) ) by A4, A5, A9, Lm3;
then (doms p) . (n + 1) = dom (t | <*n*>) by FUNCT_6:22
.= (dom t) | <*n*> by TREES_2:def_10 ;
hence ( q in (doms p) . (n + 1) & x = <*n*> ^ q ) by A12, A13, TREES_1:def_6; ::_thesis: verum
end;
assume A14: ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) ; ::_thesis: x in dom t
assume A15: not x in dom t ; ::_thesis: contradiction
then consider n being Element of NAT , q being FinSequence such that
A16: n < len (doms p) and
A17: q in (doms p) . (n + 1) and
A18: x = <*n*> ^ q by A14, TREES_1:22;
( n + 1 in dom p & ex k being Element of NAT st
( k + 1 = n + 1 & p . (n + 1) = t | <*k*> ) ) by A4, A5, A9, A16, Lm3;
then (doms p) . (n + 1) = dom (t | <*n*>) by FUNCT_6:22
.= (dom t) | <*n*> by TREES_2:def_10 ;
then reconsider q = q as Element of (dom t) | <*n*> by A17;
<*n*> in A by A6, A8, A9, A16;
then <*n*> ^ q in dom t by TREES_1:def_6;
hence contradiction by A15, A18; ::_thesis: verum
end;
then A19: dom t = tree (doms p) by TREES_3:def_15;
take p ; ::_thesis: t = (t . {}) -tree p
now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_len_p_holds_
t_|_<*n*>_=_p_._(n_+_1)
let n be Element of NAT ; ::_thesis: ( n < len p implies t | <*n*> = p . (n + 1) )
assume n < len p ; ::_thesis: t | <*n*> = p . (n + 1)
then ex m being Element of NAT st
( m + 1 = n + 1 & p . (n + 1) = t | <*m*> ) by A4, A5, Lm3;
hence t | <*n*> = p . (n + 1) ; ::_thesis: verum
end;
hence t = (t . {}) -tree p by A19, TREES_4:def_4; ::_thesis: verum
end;
registration
let t be finite DecoratedTree;
let p be Node of t;
clustert | p -> finite ;
coherence
t | p is finite ;
end;
theorem Th9: :: TREES_9:9
for t being finite Tree
for p being Element of t st t = t | p holds
p = {}
proof
let t be finite Tree; ::_thesis: for p being Element of t st t = t | p holds
p = {}
let p be Element of t; ::_thesis: ( t = t | p implies p = {} )
( p <> {} implies height t > height (t | p) ) by TREES_1:48;
hence ( t = t | p implies p = {} ) ; ::_thesis: verum
end;
registration
let D be non empty set ;
let S be non empty Subset of (FinTrees D);
cluster -> finite for Element of S;
coherence
for b1 being Element of S holds b1 is finite ;
end;
begin
definition
let t be DecoratedTree;
func Subtrees t -> set equals :: TREES_9:def 7
{ (t | p) where p is Node of t : verum } ;
coherence
{ (t | p) where p is Node of t : verum } is set ;
end;
:: deftheorem defines Subtrees TREES_9:def_7_:_
for t being DecoratedTree holds Subtrees t = { (t | p) where p is Node of t : verum } ;
registration
let t be DecoratedTree;
cluster Subtrees t -> non empty constituted-DTrees ;
coherence
( Subtrees t is constituted-DTrees & not Subtrees t is empty )
proof
set p0 = the Node of t;
set S = { (t | p) where p is Node of t : verum } ;
t | the Node of t in { (t | p) where p is Node of t : verum } ;
then reconsider S = { (t | p) where p is Node of t : verum } as non empty set ;
S is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( not x in S or x is set )
assume x in S ; ::_thesis: x is set
then ex p being Node of t st x = t | p ;
hence x is set ; ::_thesis: verum
end;
hence ( Subtrees t is constituted-DTrees & not Subtrees t is empty ) ; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let t be DecoratedTree of D;
:: original: Subtrees
redefine func Subtrees t -> non empty Subset of (Trees D);
coherence
Subtrees t is non empty Subset of (Trees D)
proof
Subtrees t c= Trees D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees t or x in Trees D )
assume x in Subtrees t ; ::_thesis: x in Trees D
then ex p being Node of t st x = t | p ;
hence x in Trees D by TREES_3:def_7; ::_thesis: verum
end;
hence Subtrees t is non empty Subset of (Trees D) ; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let t be finite DecoratedTree of D;
:: original: Subtrees
redefine func Subtrees t -> non empty Subset of (FinTrees D);
coherence
Subtrees t is non empty Subset of (FinTrees D)
proof
Subtrees t c= FinTrees D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees t or x in FinTrees D )
assume x in Subtrees t ; ::_thesis: x in FinTrees D
then ex p being Node of t st x = t | p ;
then reconsider x = x as finite DecoratedTree of D ;
dom x is finite ;
hence x in FinTrees D by TREES_3:def_8; ::_thesis: verum
end;
hence Subtrees t is non empty Subset of (FinTrees D) ; ::_thesis: verum
end;
end;
registration
let t be finite DecoratedTree;
cluster -> finite for Element of Subtrees t;
coherence
for b1 being Element of Subtrees t holds b1 is finite
proof
let x be Element of Subtrees t; ::_thesis: x is finite
x in { (t | p) where p is Node of t : verum } ;
then ex p being Node of t st x = t | p ;
hence x is finite ; ::_thesis: verum
end;
end;
theorem Th10: :: TREES_9:10
for x being set
for t being DecoratedTree holds
( x in Subtrees t iff ex n being Node of t st x = t | n ) ;
theorem Th11: :: TREES_9:11
for t being DecoratedTree holds t in Subtrees t
proof
let t be DecoratedTree; ::_thesis: t in Subtrees t
reconsider e = {} as Node of t by TREES_1:22;
t | e = t by Th1;
hence t in Subtrees t ; ::_thesis: verum
end;
theorem :: TREES_9:12
for t1, t2 being DecoratedTree st t1 is finite & Subtrees t1 = Subtrees t2 holds
t1 = t2
proof
let t1, t2 be DecoratedTree; ::_thesis: ( t1 is finite & Subtrees t1 = Subtrees t2 implies t1 = t2 )
assume that
A1: t1 is finite and
A2: Subtrees t1 = Subtrees t2 ; ::_thesis: t1 = t2
reconsider t = t1 as finite DecoratedTree by A1;
t1 in Subtrees t2 by A2, Th11;
then consider n being Node of t2 such that
A3: t1 = t2 | n ;
t2 in Subtrees t1 by A2, Th11;
then consider m being Node of t1 such that
A4: t2 = t1 | m ;
dom (t1 | m) = (dom t1) | m by TREES_2:def_10;
then reconsider p = m ^ n as Element of dom t by A4, TREES_1:def_6;
t = t | p by A3, A4, Th3;
then dom t = (dom t) | p by TREES_2:def_10;
then n = {} by Th9;
hence t1 = t2 by A3, Th1; ::_thesis: verum
end;
theorem :: TREES_9:13
for t being DecoratedTree
for n being Node of t holds Subtrees (t | n) c= Subtrees t
proof
let t be DecoratedTree; ::_thesis: for n being Node of t holds Subtrees (t | n) c= Subtrees t
let n be Node of t; ::_thesis: Subtrees (t | n) c= Subtrees t
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees (t | n) or x in Subtrees t )
assume x in Subtrees (t | n) ; ::_thesis: x in Subtrees t
then consider p being Node of (t | n) such that
A1: x = (t | n) | p ;
dom (t | n) = (dom t) | n by TREES_2:def_10;
then reconsider q = n ^ p as Node of t by TREES_1:def_6;
x = t | q by A1, Th3;
hence x in Subtrees t ; ::_thesis: verum
end;
definition
let t be DecoratedTree;
func FixedSubtrees t -> Subset of [:(dom t),(Subtrees t):] equals :: TREES_9:def 8
{ [p,(t | p)] where p is Node of t : verum } ;
coherence
{ [p,(t | p)] where p is Node of t : verum } is Subset of [:(dom t),(Subtrees t):]
proof
set S = { [p,(t | p)] where p is Node of t : verum } ;
{ [p,(t | p)] where p is Node of t : verum } c= [:(dom t),(Subtrees t):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [p,(t | p)] where p is Node of t : verum } or x in [:(dom t),(Subtrees t):] )
assume x in { [p,(t | p)] where p is Node of t : verum } ; ::_thesis: x in [:(dom t),(Subtrees t):]
then consider p being Node of t such that
A1: x = [p,(t | p)] ;
t | p in Subtrees t ;
hence x in [:(dom t),(Subtrees t):] by A1, ZFMISC_1:87; ::_thesis: verum
end;
hence { [p,(t | p)] where p is Node of t : verum } is Subset of [:(dom t),(Subtrees t):] ; ::_thesis: verum
end;
end;
:: deftheorem defines FixedSubtrees TREES_9:def_8_:_
for t being DecoratedTree holds FixedSubtrees t = { [p,(t | p)] where p is Node of t : verum } ;
registration
let t be DecoratedTree;
cluster FixedSubtrees t -> non empty ;
coherence
not FixedSubtrees t is empty
proof
set p0 = the Node of t;
set S = { [p,(t | p)] where p is Node of t : verum } ;
[ the Node of t,(t | the Node of t)] in { [p,(t | p)] where p is Node of t : verum } ;
hence not FixedSubtrees t is empty ; ::_thesis: verum
end;
end;
theorem :: TREES_9:14
for x being set
for t being DecoratedTree holds
( x in FixedSubtrees t iff ex n being Node of t st x = [n,(t | n)] ) ;
theorem Th15: :: TREES_9:15
for t being DecoratedTree holds [{},t] in FixedSubtrees t
proof
let t be DecoratedTree; ::_thesis: [{},t] in FixedSubtrees t
reconsider e = {} as Node of t by TREES_1:22;
t | e = t by Th1;
hence [{},t] in FixedSubtrees t ; ::_thesis: verum
end;
theorem :: TREES_9:16
for t1, t2 being DecoratedTree st FixedSubtrees t1 = FixedSubtrees t2 holds
t1 = t2
proof
let t1, t2 be DecoratedTree; ::_thesis: ( FixedSubtrees t1 = FixedSubtrees t2 implies t1 = t2 )
assume FixedSubtrees t1 = FixedSubtrees t2 ; ::_thesis: t1 = t2
then [{},t1] in FixedSubtrees t2 by Th15;
then consider n being Node of t2 such that
A1: [{},t1] = [n,(t2 | n)] ;
( {} = n & t1 = t2 | n ) by A1, XTUPLE_0:1;
hence t1 = t2 by Th1; ::_thesis: verum
end;
definition
let t be DecoratedTree;
let C be set ;
funcC -Subtrees t -> Subset of (Subtrees t) equals :: TREES_9:def 9
{ (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
coherence
{ (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees t)
proof
set W = { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
{ (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } c= Subtrees t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } or x in Subtrees t )
assume x in { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ; ::_thesis: x in Subtrees t
then ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) ;
hence x in Subtrees t ; ::_thesis: verum
end;
hence { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees t) ; ::_thesis: verum
end;
end;
:: deftheorem defines -Subtrees TREES_9:def_9_:_
for t being DecoratedTree
for C being set holds C -Subtrees t = { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
theorem Th17: :: TREES_9:17
for x being set
for t being DecoratedTree
for C being set holds
( x in C -Subtrees t iff ex n being Node of t st
( x = t | n & ( not n in Leaves (dom t) or t . n in C ) ) ) ;
theorem :: TREES_9:18
for t being DecoratedTree
for C being set holds
( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )
proof
let t be DecoratedTree; ::_thesis: for C being set holds
( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )
let C be set ; ::_thesis: ( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )
reconsider e = {} as Node of t by TREES_1:22;
hereby ::_thesis: ( t is root & not t . {} in C implies C -Subtrees t is empty )
assume C -Subtrees t is empty ; ::_thesis: ( t is root & not t . {} in C )
then A1: not t | e in C -Subtrees t ;
then e in Leaves (dom t) ;
hence ( t is root & not t . {} in C ) by A1, Th4; ::_thesis: verum
end;
assume that
A2: t is root and
A3: not t . {} in C ; ::_thesis: C -Subtrees t is empty
assume not C -Subtrees t is empty ; ::_thesis: contradiction
then reconsider S = C -Subtrees t as non empty Subset of (Subtrees t) ;
set s = the Element of S;
consider n being Node of t such that
the Element of S = t | n and
A4: ( not n in Leaves (dom t) or t . n in C ) by Th17;
A5: dom t = {{}} by A2, Def1, TREES_1:29;
then n = {} by TARSKI:def_1;
then e ^ <*0*> in dom t by A3, A4, TREES_1:54;
hence contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
definition
let t be finite DecoratedTree;
let C be set ;
funcC -ImmediateSubtrees t -> Function of (C -Subtrees t),((Subtrees t) *) means :: TREES_9:def 10
for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = it . d holds
d = (d . {}) -tree p;
existence
ex b1 being Function of (C -Subtrees t),((Subtrees t) *) st
for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b1 . d holds
d = (d . {}) -tree p
proof
defpred S1[ set , set ] means ex d being DecoratedTree ex p being FinSequence of Subtrees t st
( p = $2 & d = $1 & d = (d . {}) -tree p );
A1: for x being set st x in C -Subtrees t holds
ex y being set st
( y in (Subtrees t) * & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in C -Subtrees t implies ex y being set st
( y in (Subtrees t) * & S1[x,y] ) )
assume x in C -Subtrees t ; ::_thesis: ex y being set st
( y in (Subtrees t) * & S1[x,y] )
then reconsider s = x as Element of Subtrees t ;
reconsider d = s as DecoratedTree ;
consider sp being Node of t such that
A2: s = t | sp by Th10;
consider z being set , p being DTree-yielding FinSequence such that
A3: s = z -tree p by Th8;
rng p c= Subtrees t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Subtrees t )
A4: dom (t | sp) = (dom t) | sp by TREES_2:def_10;
assume x in rng p ; ::_thesis: x in Subtrees t
then consider k being Element of NAT such that
A5: ( k < len p & x = p . (k + 1) ) by Lm4;
reconsider e = {} as Node of (s | <*k*>) by TREES_1:22;
A6: x = s | <*k*> by A3, A5, TREES_4:def_4;
<*k*> ^ e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A3, A5, A6, TREES_4:11;
then reconsider q = sp ^ <*k*> as Node of t by A2, A4, TREES_1:def_6;
x = t | q by A2, A6, Th3;
hence x in Subtrees t ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of Subtrees t by FINSEQ_1:def_4;
reconsider y = p as set ;
take y ; ::_thesis: ( y in (Subtrees t) * & S1[x,y] )
thus y in (Subtrees t) * by FINSEQ_1:def_11; ::_thesis: S1[x,y]
take d ; ::_thesis: ex p being FinSequence of Subtrees t st
( p = y & d = x & d = (d . {}) -tree p )
take p ; ::_thesis: ( p = y & d = x & d = (d . {}) -tree p )
thus ( p = y & d = x & d = (d . {}) -tree p ) by A3, TREES_4:def_4; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = C -Subtrees t & rng f c= (Subtrees t) * & ( for x being set st x in C -Subtrees t holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider f = f as Function of (C -Subtrees t),((Subtrees t) *) by A7, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p
let d be DecoratedTree; ::_thesis: ( d in C -Subtrees t implies for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p )
assume d in C -Subtrees t ; ::_thesis: for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p
then ex d9 being DecoratedTree ex p being FinSequence of Subtrees t st
( p = f . d & d9 = d & d9 = (d9 . {}) -tree p ) by A7;
hence for p being FinSequence of Subtrees t st p = f . d holds
d = (d . {}) -tree p ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (C -Subtrees t),((Subtrees t) *) st ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b2 . d holds
d = (d . {}) -tree p ) holds
b1 = b2
proof
let f1, f2 be Function of (C -Subtrees t),((Subtrees t) *); ::_thesis: ( ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f2 . d holds
d = (d . {}) -tree p ) implies f1 = f2 )
assume A8: ( ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f2 . d holds
d = (d . {}) -tree p ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_C_-Subtrees_t_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in C -Subtrees t implies f1 . x = f2 . x )
assume A9: x in C -Subtrees t ; ::_thesis: f1 . x = f2 . x
then reconsider s = x as Element of Subtrees t ;
reconsider p1 = f1 . s, p2 = f2 . s as Element of (Subtrees t) * by A9, FUNCT_2:5;
( s = (s . {}) -tree p1 & s = (s . {}) -tree p2 ) by A8, A9;
hence f1 . x = f2 . x by TREES_4:15; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem defines -ImmediateSubtrees TREES_9:def_10_:_
for t being finite DecoratedTree
for C being set
for b3 being Function of (C -Subtrees t),((Subtrees t) *) holds
( b3 = C -ImmediateSubtrees t iff for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b3 . d holds
d = (d . {}) -tree p );
begin
definition
let X be non empty constituted-DTrees set ;
func Subtrees X -> set equals :: TREES_9:def 11
{ (t | p) where t is Element of X, p is Node of t : verum } ;
coherence
{ (t | p) where t is Element of X, p is Node of t : verum } is set ;
end;
:: deftheorem defines Subtrees TREES_9:def_11_:_
for X being non empty constituted-DTrees set holds Subtrees X = { (t | p) where t is Element of X, p is Node of t : verum } ;
registration
let X be non empty constituted-DTrees set ;
cluster Subtrees X -> non empty constituted-DTrees ;
coherence
( Subtrees X is constituted-DTrees & not Subtrees X is empty )
proof
set S = { (t | p) where t is Element of X, p is Node of t : verum } ;
set t = the Element of X;
set p0 = the Node of the Element of X;
the Element of X | the Node of the Element of X in { (t | p) where t is Element of X, p is Node of t : verum } ;
then reconsider S = { (t | p) where t is Element of X, p is Node of t : verum } as non empty set ;
S is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( not x in S or x is set )
assume x in S ; ::_thesis: x is set
then ex t being Element of X ex p being Node of t st x = t | p ;
hence x is set ; ::_thesis: verum
end;
hence ( Subtrees X is constituted-DTrees & not Subtrees X is empty ) ; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let X be non empty Subset of (Trees D);
:: original: Subtrees
redefine func Subtrees X -> non empty Subset of (Trees D);
coherence
Subtrees X is non empty Subset of (Trees D)
proof
Subtrees X c= Trees D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees X or x in Trees D )
assume x in Subtrees X ; ::_thesis: x in Trees D
then ex t being Element of X ex p being Node of t st x = t | p ;
hence x in Trees D by TREES_3:def_7; ::_thesis: verum
end;
hence Subtrees X is non empty Subset of (Trees D) ; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let X be non empty Subset of (FinTrees D);
:: original: Subtrees
redefine func Subtrees X -> non empty Subset of (FinTrees D);
coherence
Subtrees X is non empty Subset of (FinTrees D)
proof
Subtrees X c= FinTrees D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees X or x in FinTrees D )
assume x in Subtrees X ; ::_thesis: x in FinTrees D
then ex t being Element of X ex p being Node of t st x = t | p ;
then reconsider x = x as finite DecoratedTree of D ;
dom x is finite ;
hence x in FinTrees D by TREES_3:def_8; ::_thesis: verum
end;
hence Subtrees X is non empty Subset of (FinTrees D) ; ::_thesis: verum
end;
end;
theorem Th19: :: TREES_9:19
for x being set
for X being non empty constituted-DTrees set holds
( x in Subtrees X iff ex t being Element of X ex n being Node of t st x = t | n ) ;
theorem :: TREES_9:20
for t being DecoratedTree
for X being non empty constituted-DTrees set st t in X holds
t in Subtrees X
proof
let t be DecoratedTree; ::_thesis: for X being non empty constituted-DTrees set st t in X holds
t in Subtrees X
let X be non empty constituted-DTrees set ; ::_thesis: ( t in X implies t in Subtrees X )
assume t in X ; ::_thesis: t in Subtrees X
then reconsider t = t as Element of X ;
reconsider e = {} as Node of t by TREES_1:22;
t | e = t by Th1;
hence t in Subtrees X ; ::_thesis: verum
end;
theorem :: TREES_9:21
for X, Y being non empty constituted-DTrees set st X c= Y holds
Subtrees X c= Subtrees Y
proof
let X, Y be non empty constituted-DTrees set ; ::_thesis: ( X c= Y implies Subtrees X c= Subtrees Y )
assume A1: for x being set st x in X holds
x in Y ; :: according to TARSKI:def_3 ::_thesis: Subtrees X c= Subtrees Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees X or x in Subtrees Y )
assume x in Subtrees X ; ::_thesis: x in Subtrees Y
then consider t being Element of X, p being Node of t such that
A2: x = t | p ;
reconsider t = t as Element of Y by A1;
reconsider p = p as Node of t ;
x = t | p by A2;
hence x in Subtrees Y ; ::_thesis: verum
end;
registration
let t be DecoratedTree;
cluster{t} -> constituted-DTrees ;
coherence
{t} is constituted-DTrees by TREES_3:14;
end;
theorem :: TREES_9:22
for t being DecoratedTree holds Subtrees {t} = Subtrees t
proof
let t be DecoratedTree; ::_thesis: Subtrees {t} = Subtrees t
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Subtrees t c= Subtrees {t}
let x be set ; ::_thesis: ( x in Subtrees {t} implies x in Subtrees t )
assume x in Subtrees {t} ; ::_thesis: x in Subtrees t
then consider u being Element of {t}, p being Node of u such that
A1: x = u | p ;
u = t by TARSKI:def_1;
hence x in Subtrees t by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Subtrees t or x in Subtrees {t} )
assume x in Subtrees t ; ::_thesis: x in Subtrees {t}
then ( t in {t} & ex p being Node of t st x = t | p ) by TARSKI:def_1;
hence x in Subtrees {t} ; ::_thesis: verum
end;
theorem :: TREES_9:23
for X being non empty constituted-DTrees set holds Subtrees X = union { (Subtrees t) where t is Element of X : verum }
proof
let X be non empty constituted-DTrees set ; ::_thesis: Subtrees X = union { (Subtrees t) where t is Element of X : verum }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (Subtrees t) where t is Element of X : verum } c= Subtrees X
let x be set ; ::_thesis: ( x in Subtrees X implies x in union { (Subtrees s) where s is Element of X : verum } )
assume x in Subtrees X ; ::_thesis: x in union { (Subtrees s) where s is Element of X : verum }
then consider t being Element of X such that
A1: ex p being Node of t st x = t | p ;
( Subtrees t in { (Subtrees s) where s is Element of X : verum } & x in Subtrees t ) by A1;
hence x in union { (Subtrees s) where s is Element of X : verum } by TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Subtrees t) where t is Element of X : verum } or x in Subtrees X )
assume x in union { (Subtrees s) where s is Element of X : verum } ; ::_thesis: x in Subtrees X
then consider Y being set such that
A2: x in Y and
A3: Y in { (Subtrees s) where s is Element of X : verum } by TARSKI:def_4;
consider t being Element of X such that
A4: Y = Subtrees t by A3;
ex p being Node of t st x = t | p by A2, A4;
hence x in Subtrees X ; ::_thesis: verum
end;
definition
let X be non empty constituted-DTrees set ;
let C be set ;
funcC -Subtrees X -> Subset of (Subtrees X) equals :: TREES_9:def 12
{ (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
coherence
{ (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees X)
proof
set W = { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
{ (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } c= Subtrees X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } or x in Subtrees X )
assume x in { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ; ::_thesis: x in Subtrees X
then ex t being Element of X ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) ;
hence x in Subtrees X ; ::_thesis: verum
end;
hence { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees X) ; ::_thesis: verum
end;
end;
:: deftheorem defines -Subtrees TREES_9:def_12_:_
for X being non empty constituted-DTrees set
for C being set holds C -Subtrees X = { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
theorem Th24: :: TREES_9:24
for x, C being set
for X being non empty constituted-DTrees set holds
( x in C -Subtrees X iff ex t being Element of X ex n being Node of t st
( x = t | n & ( not n in Leaves (dom t) or t . n in C ) ) ) ;
theorem :: TREES_9:25
for C being set
for X being non empty constituted-DTrees set holds
( C -Subtrees X is empty iff for t being Element of X holds
( t is root & not t . {} in C ) )
proof
let C be set ; ::_thesis: for X being non empty constituted-DTrees set holds
( C -Subtrees X is empty iff for t being Element of X holds
( t is root & not t . {} in C ) )
let X be non empty constituted-DTrees set ; ::_thesis: ( C -Subtrees X is empty iff for t being Element of X holds
( t is root & not t . {} in C ) )
hereby ::_thesis: ( ( for t being Element of X holds
( t is root & not t . {} in C ) ) implies C -Subtrees X is empty )
assume A1: C -Subtrees X is empty ; ::_thesis: for t being Element of X holds
( t is root & not t . {} in C )
let t be Element of X; ::_thesis: ( t is root & not t . {} in C )
reconsider e = {} as Node of t by TREES_1:22;
A2: not t | e in C -Subtrees X by A1;
then e in Leaves (dom t) ;
hence ( t is root & not t . {} in C ) by A2, Th4; ::_thesis: verum
end;
assume A3: for t being Element of X holds
( t is root & not t . {} in C ) ; ::_thesis: C -Subtrees X is empty
assume not C -Subtrees X is empty ; ::_thesis: contradiction
then reconsider S = C -Subtrees X as non empty Subset of (Subtrees X) ;
set s = the Element of S;
consider t being Element of X, n being Node of t such that
the Element of S = t | n and
A4: ( not n in Leaves (dom t) or t . n in C ) by Th24;
reconsider e = {} as Node of t by TREES_1:22;
t is root by A3;
then A5: dom t = {{}} by Def1, TREES_1:29;
then n = {} by TARSKI:def_1;
then e ^ <*0*> in dom t by A3, A4, TREES_1:54;
hence contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
theorem :: TREES_9:26
for t being DecoratedTree
for C being set holds C -Subtrees {t} = C -Subtrees t
proof
let t be DecoratedTree; ::_thesis: for C being set holds C -Subtrees {t} = C -Subtrees t
let C be set ; ::_thesis: C -Subtrees {t} = C -Subtrees t
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: C -Subtrees t c= C -Subtrees {t}
let x be set ; ::_thesis: ( x in C -Subtrees {t} implies x in C -Subtrees t )
assume x in C -Subtrees {t} ; ::_thesis: x in C -Subtrees t
then consider u being Element of {t}, p being Node of u such that
A1: ( x = u | p & ( not p in Leaves (dom u) or u . p in C ) ) ;
u = t by TARSKI:def_1;
hence x in C -Subtrees t by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C -Subtrees t or x in C -Subtrees {t} )
assume x in C -Subtrees t ; ::_thesis: x in C -Subtrees {t}
then ( t in {t} & ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) ) by TARSKI:def_1;
hence x in C -Subtrees {t} ; ::_thesis: verum
end;
theorem :: TREES_9:27
for C being set
for X being non empty constituted-DTrees set holds C -Subtrees X = union { (C -Subtrees t) where t is Element of X : verum }
proof
let C be set ; ::_thesis: for X being non empty constituted-DTrees set holds C -Subtrees X = union { (C -Subtrees t) where t is Element of X : verum }
let X be non empty constituted-DTrees set ; ::_thesis: C -Subtrees X = union { (C -Subtrees t) where t is Element of X : verum }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (C -Subtrees t) where t is Element of X : verum } c= C -Subtrees X
let x be set ; ::_thesis: ( x in C -Subtrees X implies x in union { (C -Subtrees s) where s is Element of X : verum } )
assume x in C -Subtrees X ; ::_thesis: x in union { (C -Subtrees s) where s is Element of X : verum }
then consider t being Element of X such that
A1: ex n being Node of t st
( x = t | n & ( not n in Leaves (dom t) or t . n in C ) ) ;
( C -Subtrees t in { (C -Subtrees s) where s is Element of X : verum } & x in C -Subtrees t ) by A1;
hence x in union { (C -Subtrees s) where s is Element of X : verum } by TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (C -Subtrees t) where t is Element of X : verum } or x in C -Subtrees X )
assume x in union { (C -Subtrees s) where s is Element of X : verum } ; ::_thesis: x in C -Subtrees X
then consider Y being set such that
A2: x in Y and
A3: Y in { (C -Subtrees s) where s is Element of X : verum } by TARSKI:def_4;
consider t being Element of X such that
A4: Y = C -Subtrees t by A3;
ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) by A2, A4;
hence x in C -Subtrees X ; ::_thesis: verum
end;
definition
let X be non empty constituted-DTrees set ;
assume B1: for t being Element of X holds t is finite ;
let C be set ;
funcC -ImmediateSubtrees X -> Function of (C -Subtrees X),((Subtrees X) *) means :: TREES_9:def 13
for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = it . d holds
d = (d . {}) -tree p;
existence
ex b1 being Function of (C -Subtrees X),((Subtrees X) *) st
for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b1 . d holds
d = (d . {}) -tree p
proof
defpred S1[ set , set ] means ex d being DecoratedTree ex p being FinSequence of Subtrees X st
( p = $2 & d = $1 & d = (d . {}) -tree p );
A1: for x being set st x in C -Subtrees X holds
ex y being set st
( y in (Subtrees X) * & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in C -Subtrees X implies ex y being set st
( y in (Subtrees X) * & S1[x,y] ) )
assume x in C -Subtrees X ; ::_thesis: ex y being set st
( y in (Subtrees X) * & S1[x,y] )
then reconsider s = x as Element of Subtrees X ;
reconsider d = s as DecoratedTree ;
consider t being Element of X, sp being Node of t such that
A2: s = t | sp by Th19;
t is finite by B1;
then consider z being set , p being DTree-yielding FinSequence such that
A3: s = z -tree p by A2, Th8;
rng p c= Subtrees X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Subtrees X )
A4: dom (t | sp) = (dom t) | sp by TREES_2:def_10;
assume x in rng p ; ::_thesis: x in Subtrees X
then consider k being Element of NAT such that
A5: ( k < len p & x = p . (k + 1) ) by Lm4;
reconsider e = {} as Node of (s | <*k*>) by TREES_1:22;
A6: x = s | <*k*> by A3, A5, TREES_4:def_4;
<*k*> ^ e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A3, A5, A6, TREES_4:11;
then reconsider q = sp ^ <*k*> as Node of t by A2, A4, TREES_1:def_6;
x = t | q by A2, A6, Th3;
hence x in Subtrees X ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of Subtrees X by FINSEQ_1:def_4;
reconsider y = p as set ;
take y ; ::_thesis: ( y in (Subtrees X) * & S1[x,y] )
thus y in (Subtrees X) * by FINSEQ_1:def_11; ::_thesis: S1[x,y]
take d ; ::_thesis: ex p being FinSequence of Subtrees X st
( p = y & d = x & d = (d . {}) -tree p )
take p ; ::_thesis: ( p = y & d = x & d = (d . {}) -tree p )
thus ( p = y & d = x & d = (d . {}) -tree p ) by A3, TREES_4:def_4; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = C -Subtrees X & rng f c= (Subtrees X) * & ( for x being set st x in C -Subtrees X holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider f = f as Function of (C -Subtrees X),((Subtrees X) *) by A7, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f . d holds
d = (d . {}) -tree p
let d be DecoratedTree; ::_thesis: ( d in C -Subtrees X implies for p being FinSequence of Subtrees X st p = f . d holds
d = (d . {}) -tree p )
assume d in C -Subtrees X ; ::_thesis: for p being FinSequence of Subtrees X st p = f . d holds
d = (d . {}) -tree p
then ex d9 being DecoratedTree ex p being FinSequence of Subtrees X st
( p = f . d & d9 = d & d9 = (d9 . {}) -tree p ) by A7;
hence for p being FinSequence of Subtrees X st p = f . d holds
d = (d . {}) -tree p ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (C -Subtrees X),((Subtrees X) *) st ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b2 . d holds
d = (d . {}) -tree p ) holds
b1 = b2
proof
let f1, f2 be Function of (C -Subtrees X),((Subtrees X) *); ::_thesis: ( ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f2 . d holds
d = (d . {}) -tree p ) implies f1 = f2 )
assume A8: ( ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f2 . d holds
d = (d . {}) -tree p ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_C_-Subtrees_X_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in C -Subtrees X implies f1 . x = f2 . x )
assume A9: x in C -Subtrees X ; ::_thesis: f1 . x = f2 . x
then reconsider s = x as Element of Subtrees X ;
reconsider p1 = f1 . s, p2 = f2 . s as Element of (Subtrees X) * by A9, FUNCT_2:5;
( s = (s . {}) -tree p1 & s = (s . {}) -tree p2 ) by A8, A9;
hence f1 . x = f2 . x by TREES_4:15; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem defines -ImmediateSubtrees TREES_9:def_13_:_
for X being non empty constituted-DTrees set st ( for t being Element of X holds t is finite ) holds
for C being set
for b3 being Function of (C -Subtrees X),((Subtrees X) *) holds
( b3 = C -ImmediateSubtrees X iff for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = b3 . d holds
d = (d . {}) -tree p );
registration
let t be Tree;
cluster Relation-like NAT -defined NAT -valued empty Function-like finite FinSequence-like FinSubsequence-like for Element of t;
existence
ex b1 being Element of t st b1 is empty
proof
{} in t by TREES_1:22;
hence ex b1 being Element of t st b1 is empty ; ::_thesis: verum
end;
end;
theorem :: TREES_9:28
for t being finite DecoratedTree
for p being Element of dom t holds
( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )
proof
let t be finite DecoratedTree; ::_thesis: for p being Element of dom t holds
( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )
let p be Element of dom t; ::_thesis: ( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) )
( ex q being Element of dom t st
( q = p & succ (t,p) = t * (q succ) ) & rng (p succ) c= dom t ) by Def6;
then dom (succ (t,p)) = dom (p succ) by RELAT_1:27;
hence ( len (succ (t,p)) = len (p succ) & dom (succ (t,p)) = dom (p succ) ) by FINSEQ_3:29; ::_thesis: verum
end;
theorem Th29: :: TREES_9:29
for p being FinTree-yielding FinSequence
for n being empty Element of tree p holds card (succ n) = len p
proof
let p be FinTree-yielding FinSequence; ::_thesis: for n being empty Element of tree p holds card (succ n) = len p
let n be empty Element of tree p; ::_thesis: card (succ n) = len p
assume A1: not card (succ n) = len p ; ::_thesis: contradiction
percases ( card (succ n) < len p or card (succ n) > len p ) by A1, XXREAL_0:1;
supposeA2: card (succ n) < len p ; ::_thesis: contradiction
then (card (succ n)) + 1 in dom p by Lm3;
then reconsider t = p . ((card (succ n)) + 1) as finite Tree by TREES_3:23;
A3: n ^ <*(card (succ n))*> = <*(card (succ n))*> by FINSEQ_1:34;
( n in t & <*(card (succ n))*> ^ n = <*(card (succ n))*> ) by FINSEQ_1:34, TREES_1:22;
then n ^ <*(card (succ n))*> in tree p by A2, A3, TREES_3:def_15;
then n ^ <*(card (succ n))*> in succ n ;
hence contradiction by Th7; ::_thesis: verum
end;
suppose card (succ n) > len p ; ::_thesis: contradiction
then n ^ <*(len p)*> in succ n by Th7;
then n ^ <*(len p)*> in tree p ;
then <*(len p)*> in tree p by FINSEQ_1:34;
then consider i being Element of NAT , q being FinSequence such that
A4: i < len p and
q in p . (i + 1) and
A5: <*(len p)*> = <*i*> ^ q by TREES_3:def_15;
len p = <*(len p)*> . 1 by FINSEQ_1:40
.= i by A5, FINSEQ_1:41 ;
hence contradiction by A4; ::_thesis: verum
end;
end;
end;
theorem :: TREES_9:30
for t being finite DecoratedTree
for x being set
for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ (t,n) = roots p
proof
let t be finite DecoratedTree; ::_thesis: for x being set
for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ (t,n) = roots p
let x be set ; ::_thesis: for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ (t,n) = roots p
let p be DTree-yielding FinSequence; ::_thesis: ( t = x -tree p implies for n being empty Element of dom t holds succ (t,n) = roots p )
assume A1: t = x -tree p ; ::_thesis: for n being empty Element of dom t holds succ (t,n) = roots p
let n be empty Element of dom t; ::_thesis: succ (t,n) = roots p
A2: len (doms p) = len p by TREES_3:38;
now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_p)_holds_
(doms_p)_._x_is_finite_Tree
let x be set ; ::_thesis: ( x in dom (doms p) implies (doms p) . x is finite Tree )
assume x in dom (doms p) ; ::_thesis: (doms p) . x is finite Tree
then consider i being Element of NAT such that
A3: ( x = i + 1 & i < len p ) by A2, Lm1;
A4: p . x = t | <*i*> by A1, A3, TREES_4:def_4;
( n in dom (t | <*i*>) & <*i*> ^ n = <*i*> ) by FINSEQ_1:34, TREES_1:22;
then reconsider ii = <*i*> as Node of t by A1, A3, A4, TREES_4:11;
x in dom p by A3, Lm3;
then (doms p) . x = dom (t | ii) by A4, FUNCT_6:22;
hence (doms p) . x is finite Tree ; ::_thesis: verum
end;
then reconsider dp = doms p as FinTree-yielding FinSequence by TREES_3:23;
A5: dom t = tree dp by A1, TREES_4:10;
A6: ex q being Element of dom t st
( q = n & succ (t,n) = t * (q succ) ) by Def6;
rng (n succ) c= dom t ;
then dom (succ (t,n)) = dom (n succ) by A6, RELAT_1:27;
then A7: len (succ (t,n)) = len (n succ) by FINSEQ_3:29;
then A8: len (succ (t,n)) = card (succ n) by Def5
.= len p by A2, A5, Th29 ;
A9: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_p_holds_
(succ_(t,n))_._(i_+_1)_=_(roots_p)_._(i_+_1)
let i be Element of NAT ; ::_thesis: ( i < len p implies (succ (t,n)) . (i + 1) = (roots p) . (i + 1) )
assume A10: i < len p ; ::_thesis: (succ (t,n)) . (i + 1) = (roots p) . (i + 1)
then i + 1 in dom p by Lm3;
then A11: ( {} in (dom t) | <*i*> & ex T being DecoratedTree st
( T = p . (i + 1) & (roots p) . (i + 1) = T . {} ) ) by TREES_1:22, TREES_3:def_18;
p . (i + 1) = t | <*i*> by A1, A10, TREES_4:def_4;
then A12: (roots p) . (i + 1) = t . (<*i*> ^ {}) by A11, TREES_1:22, TREES_2:def_10;
i + 1 in dom (succ (t,n)) by A8, A10, Lm3;
then (succ (t,n)) . (i + 1) = t . ((n succ) . (i + 1)) by A6, FUNCT_1:12
.= t . (n ^ <*i*>) by A7, A8, A10, Def5
.= t . <*i*> by FINSEQ_1:34 ;
hence (succ (t,n)) . (i + 1) = (roots p) . (i + 1) by A12, FINSEQ_1:34; ::_thesis: verum
end;
dom (roots p) = dom p by TREES_3:def_18;
then len (roots p) = len p by FINSEQ_3:29;
hence succ (t,n) = roots p by A8, A9, Lm2; ::_thesis: verum
end;
registration
let T be finite-branching DecoratedTree;
let t be Node of T;
clusterT | t -> finite-branching ;
coherence
T | t is finite-branching
proof
let x be Element of dom (T | t); :: according to TREES_9:def_2,TREES_9:def_4 ::_thesis: succ x is finite
A2: dom (T | t) = (dom T) | t by TREES_2:def_10;
then x in (dom T) | t ;
then reconsider tx = t ^ x as Element of dom T by TREES_1:def_6;
dom T = (dom T) with-replacement (t,((dom T) | t)) by TREES_2:6;
then succ tx, succ x are_equipotent by A2, TREES_2:37;
then card (succ x) = card (succ tx) by CARD_1:5;
hence succ x is finite ; ::_thesis: verum
end;
end;
theorem :: TREES_9:31
for t being finite-branching DecoratedTree
for p being Node of t
for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)
proof
let t be finite-branching DecoratedTree; ::_thesis: for p being Node of t
for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)
let p be Node of t; ::_thesis: for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)
let q be Node of (t | p); ::_thesis: succ (t,(p ^ q)) = succ ((t | p),q)
A1: dom (t | p) = (dom t) | p by TREES_2:def_10;
then reconsider pq = p ^ q as Element of dom t by TREES_1:def_6;
reconsider q = q as Element of dom (t | p) ;
dom t = (dom t) with-replacement (p,((dom t) | p)) by TREES_2:6;
then succ pq, succ q are_equipotent by A1, TREES_2:37;
then A2: card (succ q) = card (succ pq) by CARD_1:5;
A3: ex r being Element of dom (t | p) st
( r = q & succ ((t | p),q) = (t | p) * (r succ) ) by Def6;
rng (q succ) c= dom (t | p) ;
then A4: dom (succ ((t | p),q)) = dom (q succ) by A3, RELAT_1:27;
A5: ex q being Element of dom t st
( q = pq & succ (t,pq) = t * (q succ) ) by Def6;
rng (pq succ) c= dom t ;
then A6: dom (succ (t,pq)) = dom (pq succ) by A5, RELAT_1:27;
A7: len (q succ) = card (succ q) by Def5;
A8: len (pq succ) = card (succ pq) by Def5;
then A9: dom (pq succ) = dom (q succ) by A7, A2, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(q_succ)_holds_
(succ_(t,pq))_._i_=_(succ_((t_|_p),q))_._i
let i be Nat; ::_thesis: ( i in dom (q succ) implies (succ (t,pq)) . i = (succ ((t | p),q)) . i )
assume A10: i in dom (q succ) ; ::_thesis: (succ (t,pq)) . i = (succ ((t | p),q)) . i
then consider k being Element of NAT such that
A11: i = k + 1 and
A12: k < len (q succ) by Lm1;
A13: q ^ <*k*> in succ q by A7, A12, Th7;
thus (succ (t,pq)) . i = t . ((pq succ) . i) by A5, A9, A6, A10, FUNCT_1:12
.= t . (pq ^ <*k*>) by A8, A7, A2, A11, A12, Def5
.= t . (p ^ (q ^ <*k*>)) by FINSEQ_1:32
.= (t | p) . (q ^ <*k*>) by A1, A13, TREES_2:def_10
.= (t | p) . ((q succ) . i) by A11, A12, Def5
.= (succ ((t | p),q)) . i by A3, A4, A10, FUNCT_1:12 ; ::_thesis: verum
end;
hence succ (t,(p ^ q)) = succ ((t | p),q) by A9, A6, A4, FINSEQ_1:13; ::_thesis: verum
end;
begin
theorem Th32: :: TREES_9:32
for n being Element of NAT
for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
proof
let n be Element of NAT ; ::_thesis: for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
let r be FinSequence; ::_thesis: ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
r | (Seg n) is FinSequence by FINSEQ_1:15;
then consider q being FinSequence such that
A1: q = r | (Seg n) ;
q is_a_prefix_of r by A1, TREES_1:def_1;
hence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r ) by A1; ::_thesis: verum
end;
theorem Th33: :: TREES_9:33
for D being non empty set
for r being FinSequence of D
for r1, r2 being FinSequence
for k being Element of NAT st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
proof
let D be non empty set ; ::_thesis: for r being FinSequence of D
for r1, r2 being FinSequence
for k being Element of NAT st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let r be FinSequence of D; ::_thesis: for r1, r2 being FinSequence
for k being Element of NAT st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let r1, r2 be FinSequence; ::_thesis: for k being Element of NAT st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let k be Element of NAT ; ::_thesis: ( k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) implies ex x being Element of D st r1 = r2 ^ <*x*> )
assume that
A1: k + 1 <= len r and
A2: r1 = r | (Seg (k + 1)) and
A3: r2 = r | (Seg k) ; ::_thesis: ex x being Element of D st r1 = r2 ^ <*x*>
k < len r by A1, NAT_1:13;
then A4: len r2 = k by A3, FINSEQ_1:17;
r2 is_a_prefix_of r by A3, TREES_1:def_1;
then A5: ex q2 being FinSequence st r = r2 ^ q2 by TREES_1:1;
then reconsider r99 = r2 as FinSequence of D by FINSEQ_1:36;
r1 is_a_prefix_of r by A2, TREES_1:def_1;
then A6: ex q1 being FinSequence st r = r1 ^ q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
A7: len r1 = k + 1 by A1, A2, FINSEQ_1:17;
A8: now__::_thesis:_not_r9_is_a_prefix_of_r99
assume r9 is_a_prefix_of r99 ; ::_thesis: contradiction
then k + 1 <= k + 0 by A7, A4, NAT_1:43;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
r9,r99 are_c=-comparable by A6, A5, TREES_A:1;
then r99 is_a_prefix_of r9 by A8, XBOOLE_0:def_9;
then consider s being FinSequence such that
A9: r9 = r99 ^ s by TREES_1:1;
reconsider s = s as FinSequence of D by A9, FINSEQ_1:36;
A10: len s = 1
proof
consider m being Element of NAT such that
A11: m = len s ;
k + 1 = k + m by A7, A4, A9, A11, FINSEQ_1:22;
hence len s = 1 by A11; ::_thesis: verum
end;
consider x being set such that
A12: x = s . 1 ;
1 in {1} by TARSKI:def_1;
then 1 in dom s by A10, FINSEQ_1:2, FINSEQ_1:def_3;
then A13: x in rng s by A12, FUNCT_1:def_3;
s = <*x*> by A10, A12, FINSEQ_1:40;
hence ex x being Element of D st r1 = r2 ^ <*x*> by A9, A13; ::_thesis: verum
end;
theorem Th34: :: TREES_9:34
for D being non empty set
for r being FinSequence of D
for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
proof
let D be non empty set ; ::_thesis: for r being FinSequence of D
for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
let r be FinSequence of D; ::_thesis: for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
let r1 be FinSequence; ::_thesis: ( 1 <= len r & r1 = r | (Seg 1) implies ex x being Element of D st r1 = <*x*> )
assume that
A1: 1 <= len r and
A2: r1 = r | (Seg 1) ; ::_thesis: ex x being Element of D st r1 = <*x*>
consider x being set such that
A3: x = r1 . 1 ;
1 in {1} by TARSKI:def_1;
then 1 in dom r1 by A1, A2, FINSEQ_1:2, FINSEQ_1:17;
then A4: x in rng r1 by A3, FUNCT_1:def_3;
len r1 = 1 by A1, A2, FINSEQ_1:17;
then A5: r1 = <*x*> by A3, FINSEQ_1:40;
r1 is_a_prefix_of r by A2, TREES_1:def_1;
then ex q1 being FinSequence st r = r1 ^ q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
rng r9 c= D ;
hence ex x being Element of D st r1 = <*x*> by A5, A4; ::_thesis: verum
end;
theorem :: TREES_9:35
for T being DecoratedTree
for p being FinSequence of NAT holds T . p = (T | p) . {}
proof
let T be DecoratedTree; ::_thesis: for p being FinSequence of NAT holds T . p = (T | p) . {}
let p be FinSequence of NAT ; ::_thesis: T . p = (T | p) . {}
<*> NAT in (dom T) | p by TREES_1:22;
then (T | p) . (<*> NAT) = T . (p ^ (<*> NAT)) by TREES_2:def_10
.= T . p by FINSEQ_1:34 ;
hence T . p = (T | p) . {} ; ::_thesis: verum
end;
theorem Th36: :: TREES_9:36
for T being finite-branching DecoratedTree
for t being Element of dom T holds succ (T,t) = T * (t succ)
proof
let T be finite-branching DecoratedTree; ::_thesis: for t being Element of dom T holds succ (T,t) = T * (t succ)
let t be Element of dom T; ::_thesis: succ (T,t) = T * (t succ)
ex q being Element of dom T st
( q = t & succ (T,t) = T * (q succ) ) by Def6;
hence succ (T,t) = T * (t succ) ; ::_thesis: verum
end;
theorem Th37: :: TREES_9:37
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (T * (t succ)) = dom (t succ)
proof
let T be finite-branching DecoratedTree; ::_thesis: for t being Element of dom T holds dom (T * (t succ)) = dom (t succ)
let t be Element of dom T; ::_thesis: dom (T * (t succ)) = dom (t succ)
rng (t succ) c= dom T ;
hence dom (T * (t succ)) = dom (t succ) by RELAT_1:27; ::_thesis: verum
end;
theorem Th38: :: TREES_9:38
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (succ (T,t)) = dom (t succ)
proof
let T be finite-branching DecoratedTree; ::_thesis: for t being Element of dom T holds dom (succ (T,t)) = dom (t succ)
let t be Element of dom T; ::_thesis: dom (succ (T,t)) = dom (t succ)
thus dom (succ (T,t)) = dom (T * (t succ)) by Th36
.= dom (t succ) by Th37 ; ::_thesis: verum
end;
theorem Th39: :: TREES_9:39
for T being finite-branching DecoratedTree
for t being Element of dom T
for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )
proof
let T be finite-branching DecoratedTree; ::_thesis: for t being Element of dom T
for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )
let t be Element of dom T; ::_thesis: for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )
let n be Element of NAT ; ::_thesis: ( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )
now__::_thesis:_(_t_^_<*n*>_in_dom_T_implies_n_+_1_in_dom_(t_succ)_)
assume t ^ <*n*> in dom T ; ::_thesis: n + 1 in dom (t succ)
then t ^ <*n*> in succ t ;
then n < card (succ t) by Th7;
then n < len (t succ) by Def5;
then A1: n + 1 <= len (t succ) by NAT_1:13;
0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:6;
then n + 1 in Seg (len (t succ)) by A1, FINSEQ_1:1;
hence n + 1 in dom (t succ) by FINSEQ_1:def_3; ::_thesis: verum
end;
hence ( t ^ <*n*> in dom T implies n + 1 in dom (t succ) ) ; ::_thesis: ( n + 1 in dom (t succ) implies t ^ <*n*> in dom T )
assume n + 1 in dom (t succ) ; ::_thesis: t ^ <*n*> in dom T
then n + 1 in Seg (len (t succ)) by FINSEQ_1:def_3;
then n + 1 <= len (t succ) by FINSEQ_1:1;
then n < len (t succ) by NAT_1:13;
then n < card (succ t) by Def5;
then t ^ <*n*> in succ t by Th7;
hence t ^ <*n*> in dom T ; ::_thesis: verum
end;
theorem Th40: :: TREES_9:40
for T being finite-branching DecoratedTree
for x being FinSequence
for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
proof
let T be finite-branching DecoratedTree; ::_thesis: for x being FinSequence
for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
let x be FinSequence; ::_thesis: for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
let n be Element of NAT ; ::_thesis: ( x ^ <*n*> in dom T implies T . (x ^ <*n*>) = (succ (T,x)) . (n + 1) )
assume A1: x ^ <*n*> in dom T ; ::_thesis: T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
x is_a_prefix_of x ^ <*n*> by TREES_1:1;
then x in dom T by A1, TREES_1:20;
then consider q being Element of dom T such that
A2: q = x and
A3: succ (T,x) = T * (q succ) by Def6;
A4: n + 1 in dom (q succ) by A1, A2, Th39;
then n + 1 in Seg (len (q succ)) by FINSEQ_1:def_3;
then n + 1 <= len (q succ) by FINSEQ_1:1;
then A5: n < len (q succ) by NAT_1:13;
n + 1 in dom (T * (q succ)) by A4, Th37;
then (succ (T,x)) . (n + 1) = T . ((q succ) . (n + 1)) by A3, FUNCT_1:12
.= T . (x ^ <*n*>) by A2, A5, Def5 ;
hence T . (x ^ <*n*>) = (succ (T,x)) . (n + 1) ; ::_thesis: verum
end;
theorem :: TREES_9:41
for T being finite-branching DecoratedTree
for x9, x being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))
proof
let T be finite-branching DecoratedTree; ::_thesis: for x9, x being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))
let x9, x be Element of dom T; ::_thesis: ( x9 in succ x implies T . x9 in rng (succ (T,x)) )
assume x9 in succ x ; ::_thesis: T . x9 in rng (succ (T,x))
then consider n being Element of NAT such that
A1: x9 = x ^ <*n*> and
x ^ <*n*> in dom T ;
A2: T . x9 = (succ (T,x)) . (n + 1) by A1, Th40;
dom (succ (T,x)) = dom (T * (x succ)) by Th36
.= dom (x succ) by Th37 ;
then n + 1 in dom (succ (T,x)) by A1, Th39;
hence T . x9 in rng (succ (T,x)) by A2, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: TREES_9:42
for T being finite-branching DecoratedTree
for x being Element of dom T
for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
proof
let T be finite-branching DecoratedTree; ::_thesis: for x being Element of dom T
for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
let x be Element of dom T; ::_thesis: for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
let y9 be set ; ::_thesis: ( y9 in rng (succ (T,x)) implies ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x ) )
consider k being Nat such that
A1: dom (succ (T,x)) = Seg k by FINSEQ_1:def_2;
assume y9 in rng (succ (T,x)) ; ::_thesis: ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
then consider n9 being set such that
A2: n9 in dom (succ (T,x)) and
A3: y9 = (succ (T,x)) . n9 by FUNCT_1:def_3;
Seg k = { m where m is Element of NAT : ( 1 <= m & m <= k ) } by FINSEQ_1:def_1;
then consider m9 being Element of NAT such that
A4: n9 = m9 and
A5: 1 <= m9 and
m9 <= k by A2, A1;
m9 <> 0 by A5;
then consider n being Nat such that
A6: n + 1 = m9 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
n + 1 in dom (x succ) by A2, A4, A6, Th38;
then x ^ <*n*> in dom T by Th39;
then consider x9 being Element of dom T such that
A7: x9 = x ^ <*n*> ;
A8: x9 in succ x by A7;
y9 = T . x9 by A3, A4, A6, A7, Th40;
hence ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x ) by A8; ::_thesis: verum
end;
scheme :: TREES_9:sch 2
ExDecTrees{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> FinSequence of F1() } :
ex T being finite-branching DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T
for w being Element of F1() st w = T . t holds
succ (T,t) = F3(w) ) )
proof
defpred S1[ set , set ] means ( ( len F3($1) = 0 & $2 = {} ) or ( len F3($1) <> 0 & ex m being Element of NAT st
( m + 1 = len F3($1) & $2 = {0} \/ (Seg m) ) ) );
A1: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] )
assume x in F1() ; ::_thesis: ex y being set st S1[x,y]
percases ( len F3(x) = 0 or len F3(x) <> 0 ) ;
suppose len F3(x) = 0 ; ::_thesis: ex y being set st S1[x,y]
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
suppose len F3(x) <> 0 ; ::_thesis: ex y being set st S1[x,y]
then consider m being Nat such that
A2: m + 1 = len F3(x) by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
ex y being set st y = {0} \/ (Seg m) ;
hence ex y being set st S1[x,y] by A2; ::_thesis: verum
end;
end;
end;
ex F being Function st
( dom F = F1() & ( for x being set st x in F1() holds
S1[x,F . x] ) ) from CLASSES1:sch_1(A1);
then consider F being Function such that
A3: for x being set holds
( not x in F1() or ( len F3(x) = 0 & F . x = {} ) or ( len F3(x) <> 0 & ex m being Element of NAT st
( m + 1 = len F3(x) & F . x = {0} \/ (Seg m) ) ) ) ;
deffunc H1( set ) -> set = F . $1;
A4: for k being Element of NAT
for x being set st x in F1() holds
( k in H1(x) iff k + 1 in Seg (len F3(x)) )
proof
let k be Element of NAT ; ::_thesis: for x being set st x in F1() holds
( k in H1(x) iff k + 1 in Seg (len F3(x)) )
let x be set ; ::_thesis: ( x in F1() implies ( k in H1(x) iff k + 1 in Seg (len F3(x)) ) )
assume A5: x in F1() ; ::_thesis: ( k in H1(x) iff k + 1 in Seg (len F3(x)) )
now__::_thesis:_(_k_in_H1(x)_implies_k_+_1_in_Seg_(len_F3(x))_)
assume A6: k in H1(x) ; ::_thesis: k + 1 in Seg (len F3(x))
then consider m being Element of NAT such that
A7: m + 1 = len F3(x) and
A8: F . x = {0} \/ (Seg m) by A3, A5;
( 0 <= k & k <= m )
proof
percases ( k in {0} or k in Seg m ) by A6, A8, XBOOLE_0:def_3;
suppose k in {0} ; ::_thesis: ( 0 <= k & k <= m )
then k = 0 by TARSKI:def_1;
hence ( 0 <= k & k <= m ) by NAT_1:2; ::_thesis: verum
end;
supposeA9: k in Seg m ; ::_thesis: ( 0 <= k & k <= m )
then 0 + 1 <= k by FINSEQ_1:1;
hence ( 0 <= k & k <= m ) by A9, FINSEQ_1:1, NAT_1:13; ::_thesis: verum
end;
end;
end;
then ( 0 + 1 <= k + 1 & k + 1 <= m + 1 ) by XREAL_1:6;
hence k + 1 in Seg (len F3(x)) by A7, FINSEQ_1:1; ::_thesis: verum
end;
hence ( k in H1(x) implies k + 1 in Seg (len F3(x)) ) ; ::_thesis: ( k + 1 in Seg (len F3(x)) implies k in H1(x) )
assume A10: k + 1 in Seg (len F3(x)) ; ::_thesis: k in H1(x)
then len F3(x) <> 0 ;
then consider m being Element of NAT such that
A11: m + 1 = len F3(x) and
A12: F . x = {0} \/ (Seg m) by A3, A5;
k in {0} \/ (Seg m)
proof
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: k in {0} \/ (Seg m)
then k in {0} by TARSKI:def_1;
hence k in {0} \/ (Seg m) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose k <> 0 ; ::_thesis: k in {0} \/ (Seg m)
then 0 < k by NAT_1:3;
then A13: 0 + 1 <= k by NAT_1:13;
k + 1 <= len F3(x) by A10, FINSEQ_1:1;
then k <= m by A11, XREAL_1:6;
then k in Seg m by A13, FINSEQ_1:1;
hence k in {0} \/ (Seg m) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence k in H1(x) by A12; ::_thesis: verum
end;
A14: for T being finite-branching DecoratedTree
for x being set
for t being Element of dom T st x in F1() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H1(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) }
proof
let T be finite-branching DecoratedTree; ::_thesis: for x being set
for t being Element of dom T st x in F1() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H1(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) }
let x be set ; ::_thesis: for t being Element of dom T st x in F1() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H1(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) }
let t be Element of dom T; ::_thesis: ( x in F1() implies { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } )
assume A15: x in F1() ; ::_thesis: { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) }
thus { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } c= { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } :: according to XBOOLE_0:def_10 ::_thesis: { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } c= { (t ^ <*k*>) where k is Element of NAT : k in H1(x) }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } or y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } )
assume y in { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } ; ::_thesis: y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) }
then consider k being Element of NAT such that
A16: y = t ^ <*k*> and
A17: k in H1(x) ;
k + 1 in Seg (len F3(x)) by A4, A15, A17;
hence y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } by A16; ::_thesis: verum
end;
thus { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } c= { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } or y in { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } )
assume y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F3(x)) } ; ::_thesis: y in { (t ^ <*k*>) where k is Element of NAT : k in H1(x) }
then consider m being Element of NAT such that
A18: y = t ^ <*m*> and
A19: m + 1 in Seg (len F3(x)) ;
m in H1(x) by A4, A15, A19;
hence y in { (t ^ <*k*>) where k is Element of NAT : k in H1(x) } by A18; ::_thesis: verum
end;
end;
defpred S2[ set , set ] means ex x being set ex n being Element of NAT st
( x in F1() & $1 = [x,n] & ( ( n in H1(x) & $2 = F3(x) . (n + 1) ) or ( not n in H1(x) & $2 = F2() ) ) );
A20: for c being Element of [:F1(),NAT:] ex y being Element of F1() st S2[c,y]
proof
let c be Element of [:F1(),NAT:]; ::_thesis: ex y being Element of F1() st S2[c,y]
( c `1 in F1() & c `2 in NAT ) by MCART_1:10;
then consider x being Element of F1(), n being Element of NAT such that
A21: ( x = c `1 & n = c `2 ) ;
A22: c = [x,n] by A21, MCART_1:21;
percases ( n in H1(x) or not n in H1(x) ) ;
supposeA23: n in H1(x) ; ::_thesis: ex y being Element of F1() st S2[c,y]
then n + 1 in Seg (len F3(x)) by A4;
then n + 1 in dom F3(x) by FINSEQ_1:def_3;
then A24: F3(x) . (n + 1) in rng F3(x) by FUNCT_1:def_3;
thus ex y being Element of F1() st S2[c,y] by A22, A23, A24; ::_thesis: verum
end;
suppose not n in H1(x) ; ::_thesis: ex y being Element of F1() st S2[c,y]
hence ex y being Element of F1() st S2[c,y] by A22; ::_thesis: verum
end;
end;
end;
ex S being Function of [:F1(),NAT:],F1() st
for c being Element of [:F1(),NAT:] holds S2[c,S . c] from FUNCT_2:sch_3(A20);
then consider S being Function of [:F1(),NAT:],F1() such that
A25: for c being Element of [:F1(),NAT:] holds S2[c,S . c] ;
A26: for n being Element of NAT
for x being set
for m being Element of NAT st m + 1 = len F3(x) & x in F1() holds
( n in H1(x) iff ( 0 <= n & n <= m ) )
proof
let n be Element of NAT ; ::_thesis: for x being set
for m being Element of NAT st m + 1 = len F3(x) & x in F1() holds
( n in H1(x) iff ( 0 <= n & n <= m ) )
let x be set ; ::_thesis: for m being Element of NAT st m + 1 = len F3(x) & x in F1() holds
( n in H1(x) iff ( 0 <= n & n <= m ) )
let m be Element of NAT ; ::_thesis: ( m + 1 = len F3(x) & x in F1() implies ( n in H1(x) iff ( 0 <= n & n <= m ) ) )
assume that
A27: m + 1 = len F3(x) and
A28: x in F1() ; ::_thesis: ( n in H1(x) iff ( 0 <= n & n <= m ) )
thus ( n in H1(x) implies ( 0 <= n & n <= m ) ) ::_thesis: ( 0 <= n & n <= m implies n in H1(x) )
proof
A29: ex k being Element of NAT st
( k + 1 = len F3(x) & H1(x) = {0} \/ (Seg k) ) by A3, A27, A28;
assume A30: n in H1(x) ; ::_thesis: ( 0 <= n & n <= m )
percases ( n in {0} or n in Seg m ) by A27, A30, A29, XBOOLE_0:def_3;
suppose n in {0} ; ::_thesis: ( 0 <= n & n <= m )
then n = 0 by TARSKI:def_1;
hence ( 0 <= n & n <= m ) by NAT_1:2; ::_thesis: verum
end;
supposeA31: n in Seg m ; ::_thesis: ( 0 <= n & n <= m )
then 1 <= n by FINSEQ_1:1;
hence ( 0 <= n & n <= m ) by A31, FINSEQ_1:1, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
thus ( 0 <= n & n <= m implies n in H1(x) ) ::_thesis: verum
proof
assume that
0 <= n and
A32: n <= m ; ::_thesis: n in H1(x)
A33: ex k being Element of NAT st
( k + 1 = len F3(x) & H1(x) = {0} \/ (Seg k) ) by A3, A27, A28;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: n in H1(x)
then n in {0} by TARSKI:def_1;
hence n in H1(x) by A33, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: n in H1(x)
then 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
then n in Seg m by A32, FINSEQ_1:1;
hence n in H1(x) by A27, A33, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
A34: for d being Element of F1()
for k1, k2 being Element of NAT st k1 <= k2 & k2 in H1(d) holds
k1 in H1(d)
proof
let d be Element of F1(); ::_thesis: for k1, k2 being Element of NAT st k1 <= k2 & k2 in H1(d) holds
k1 in H1(d)
let k1, k2 be Element of NAT ; ::_thesis: ( k1 <= k2 & k2 in H1(d) implies k1 in H1(d) )
assume that
A35: k1 <= k2 and
A36: k2 in H1(d) ; ::_thesis: k1 in H1(d)
ex m being Element of NAT st
( m + 1 = len F3(d) & F . d = {0} \/ (Seg m) ) by A3, A36;
then consider m being Element of NAT such that
A37: m + 1 = len F3(d) ;
k2 <= m by A26, A36, A37;
then ( 0 <= k1 & k1 <= m ) by A35, NAT_1:2, XXREAL_0:2;
hence k1 in H1(d) by A26, A37; ::_thesis: verum
end;
consider T being DecoratedTree of F1() such that
A38: ( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in H1(T . t) } & ( for n being Element of NAT st n in H1(T . t) holds
T . (t ^ <*n*>) = S . ((T . t),n) ) ) ) ) from TREES_2:sch_8(A34);
for t being Element of dom T holds succ t is finite
proof
let t be Element of dom T; ::_thesis: succ t is finite
defpred S3[ set , set ] means ex m being Element of NAT st
( m + 1 = $1 & $2 = t ^ <*m*> );
A39: for k being Nat st k in Seg (len F3((T . t))) holds
ex x being set st S3[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len F3((T . t))) implies ex x being set st S3[k,x] )
assume k in Seg (len F3((T . t))) ; ::_thesis: ex x being set st S3[k,x]
then k <> 0 by FINSEQ_1:1;
then consider m being Nat such that
A40: m + 1 = k by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
ex x being set st x = t ^ <*m*> ;
hence ex x being set st S3[k,x] by A40; ::_thesis: verum
end;
ex L being FinSequence st
( dom L = Seg (len F3((T . t))) & ( for k being Nat st k in Seg (len F3((T . t))) holds
S3[k,L . k] ) ) from FINSEQ_1:sch_1(A39);
then consider L being FinSequence such that
A41: dom L = Seg (len F3((T . t))) and
A42: for k being Nat st k in Seg (len F3((T . t))) holds
S3[k,L . k] ;
A43: for k being Element of NAT st 1 <= k + 1 & k + 1 <= len F3((T . t)) holds
L . (k + 1) = t ^ <*k*>
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k + 1 & k + 1 <= len F3((T . t)) implies L . (k + 1) = t ^ <*k*> )
assume ( 1 <= k + 1 & k + 1 <= len F3((T . t)) ) ; ::_thesis: L . (k + 1) = t ^ <*k*>
then k + 1 in Seg (len F3((T . t))) by FINSEQ_1:1;
then ex m being Element of NAT st
( m + 1 = k + 1 & L . (k + 1) = t ^ <*m*> ) by A42;
hence L . (k + 1) = t ^ <*k*> ; ::_thesis: verum
end;
A44: succ t = { (t ^ <*k*>) where k is Element of NAT : k in H1(T . t) } by A38;
succ t c= rng L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in rng L )
assume x in succ t ; ::_thesis: x in rng L
then consider k being Element of NAT such that
A45: x = t ^ <*k*> and
A46: k in H1(T . t) by A44;
A47: k + 1 in Seg (len F3((T . t))) by A4, A46;
then ( 1 <= k + 1 & k + 1 <= len F3((T . t)) ) by FINSEQ_1:1;
then L . (k + 1) = t ^ <*k*> by A43;
hence x in rng L by A41, A45, A47, FUNCT_1:def_3; ::_thesis: verum
end;
hence succ t is finite ; ::_thesis: verum
end;
then dom T is finite-branching by Def2;
then reconsider T = T as finite-branching DecoratedTree of F1() by Def4;
A48: for n being Element of NAT
for x being set st x in F1() & n in H1(x) holds
S . (x,n) = F3(x) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for x being set st x in F1() & n in H1(x) holds
S . (x,n) = F3(x) . (n + 1)
let x be set ; ::_thesis: ( x in F1() & n in H1(x) implies S . (x,n) = F3(x) . (n + 1) )
assume that
A49: x in F1() and
A50: n in H1(x) ; ::_thesis: S . (x,n) = F3(x) . (n + 1)
( [x,n] `1 = x & [x,n] `2 = n ) ;
then [x,n] in [:F1(),NAT:] by A49, MCART_1:11;
then consider c being Element of [:F1(),NAT:] such that
A51: c = [x,n] ;
consider x9 being set , n9 being Element of NAT such that
x9 in F1() and
A52: c = [x9,n9] and
A53: ( ( n9 in H1(x9) & S . c = F3(x9) . (n9 + 1) ) or ( not n9 in H1(x9) & S . c = F2() ) ) by A25;
x9 = x by A51, A52, XTUPLE_0:1;
hence S . (x,n) = F3(x) . (n + 1) by A50, A51, A52, A53, XTUPLE_0:1; ::_thesis: verum
end;
now__::_thesis:_for_t_being_Element_of_dom_T
for_w_being_Element_of_F1()_st_w_=_T_._t_holds_
succ_(T,t)_=_F3(w)
let t be Element of dom T; ::_thesis: for w being Element of F1() st w = T . t holds
succ (T,t) = F3(w)
let w be Element of F1(); ::_thesis: ( w = T . t implies succ (T,t) = F3(w) )
assume A54: w = T . t ; ::_thesis: succ (T,t) = F3(w)
succ t = { (t ^ <*k*>) where k is Element of NAT : k in H1(w) } by A38, A54;
then A55: succ t = { (t ^ <*k*>) where k is Element of NAT : k + 1 in Seg (len F3(w)) } by A14;
A56: dom F3(w) = Seg (len F3(w)) by FINSEQ_1:def_3;
A57: dom (t succ) = Seg (len (t succ)) by FINSEQ_1:def_3;
A58: dom (t succ) c= dom F3(w)
proof
let n9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not n9 in dom (t succ) or n9 in dom F3(w) )
A59: Seg (len (t succ)) = { k where k is Element of NAT : ( 1 <= k & k <= len (t succ) ) } by FINSEQ_1:def_1;
assume n9 in dom (t succ) ; ::_thesis: n9 in dom F3(w)
then consider m being Element of NAT such that
A60: n9 = m and
A61: 1 <= m and
A62: m <= len (t succ) by A57, A59;
0 <> m by A61;
then consider n being Nat such that
A63: m = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
n + 1 in dom (t succ) by A57, A59, A61, A62, A63;
then t ^ <*n*> in dom T by Th39;
then t ^ <*n*> in succ t ;
then consider k being Element of NAT such that
A64: t ^ <*k*> = t ^ <*n*> and
A65: k + 1 in Seg (len F3(w)) by A55;
<*k*> = <*n*> by A64, FINSEQ_1:33;
hence n9 in dom F3(w) by A56, A60, A63, A65, TREES_1:5; ::_thesis: verum
end;
dom F3(w) c= dom (t succ)
proof
let n9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not n9 in dom F3(w) or n9 in dom (t succ) )
A66: Seg (len F3(w)) = { k where k is Element of NAT : ( 1 <= k & k <= len F3(w) ) } by FINSEQ_1:def_1;
assume n9 in dom F3(w) ; ::_thesis: n9 in dom (t succ)
then consider m being Element of NAT such that
A67: n9 = m and
A68: 1 <= m and
A69: m <= len F3(w) by A56, A66;
0 <> m by A68;
then consider n being Nat such that
A70: m = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
n + 1 in Seg (len F3(w)) by A66, A68, A69, A70;
then t ^ <*n*> in succ t by A55;
hence n9 in dom (t succ) by A67, A70, Th39; ::_thesis: verum
end;
then A71: dom F3(w) = dom (t succ) by A58, XBOOLE_0:def_10;
then A72: dom (succ (T,t)) = dom F3(w) by Th38;
for m being Nat st m in dom (succ (T,t)) holds
(succ (T,t)) . m = F3(w) . m
proof
let m be Nat; ::_thesis: ( m in dom (succ (T,t)) implies (succ (T,t)) . m = F3(w) . m )
A73: Seg (len F3(w)) = { k where k is Element of NAT : ( 1 <= k & k <= len F3(w) ) } by FINSEQ_1:def_1;
assume A74: m in dom (succ (T,t)) ; ::_thesis: (succ (T,t)) . m = F3(w) . m
then A75: m in Seg (len F3(w)) by A72, FINSEQ_1:def_3;
then len F3(w) <> 0 ;
then consider l being Element of NAT such that
A76: l + 1 = len F3((T . t)) and
A77: F . (T . t) = {0} \/ (Seg l) by A3, A54;
consider k being Element of NAT such that
A78: m = k and
A79: 1 <= k and
A80: k <= len F3(w) by A75, A73;
0 <> k by A79;
then consider n being Nat such that
A81: m = n + 1 by A78, NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A82: n <= l by A54, A78, A80, A81, A76, XREAL_1:6;
A83: n in {0} \/ (Seg l)
proof
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: n in {0} \/ (Seg l)
then n in {0} by TARSKI:def_1;
hence n in {0} \/ (Seg l) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: n in {0} \/ (Seg l)
then 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
then n in Seg l by A82, FINSEQ_1:1;
hence n in {0} \/ (Seg l) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
n + 1 in dom (t succ) by A74, A81, Th38;
then t ^ <*n*> in dom T by Th39;
then (succ (T,t)) . (n + 1) = T . (t ^ <*n*>) by Th40
.= S . ((T . t),n) by A38, A77, A83
.= F3(w) . (n + 1) by A48, A54, A77, A83 ;
hence (succ (T,t)) . m = F3(w) . m by A81; ::_thesis: verum
end;
hence succ (T,t) = F3(w) by A71, Th38, FINSEQ_1:13; ::_thesis: verum
end;
hence ex T being finite-branching DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T
for w being Element of F1() st w = T . t holds
succ (T,t) = F3(w) ) ) by A38; ::_thesis: verum
end;
theorem Th43: :: TREES_9:43
for T being Tree
for t being Element of T holds ProperPrefixes t is finite Chain of T
proof
let T be Tree; ::_thesis: for t being Element of T holds ProperPrefixes t is finite Chain of T
let t be Element of T; ::_thesis: ProperPrefixes t is finite Chain of T
( ProperPrefixes t c= T & ( for p, q being FinSequence of NAT st p in ProperPrefixes t & q in ProperPrefixes t holds
p,q are_c=-comparable ) ) by TREES_1:18, TREES_1:def_3;
hence ProperPrefixes t is finite Chain of T by TREES_2:def_3; ::_thesis: verum
end;
theorem Th44: :: TREES_9:44
for T being Tree holds T -level 0 = {{}}
proof
let T be Tree; ::_thesis: T -level 0 = {{}}
A1: {{}} c= { w where w is Element of T : len w = 0 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in { w where w is Element of T : len w = 0 } )
assume x in {{}} ; ::_thesis: x in { w where w is Element of T : len w = 0 }
then A2: x = {} by TARSKI:def_1;
{} in T by TREES_1:22;
then consider t being Element of T such that
A3: t = {} ;
len t = 0 by A3;
hence x in { w where w is Element of T : len w = 0 } by A2, A3; ::_thesis: verum
end;
{ w where w is Element of T : len w = 0 } c= {{}}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of T : len w = 0 } or x in {{}} )
assume x in { w where w is Element of T : len w = 0 } ; ::_thesis: x in {{}}
then consider w being Element of T such that
A4: w = x and
A5: len w = 0 ;
w = {} by A5;
hence x in {{}} by A4, TARSKI:def_1; ::_thesis: verum
end;
hence T -level 0 = {{}} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th45: :: TREES_9:45
for n being Element of NAT
for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
proof
let n be Element of NAT ; ::_thesis: for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
let T be Tree; ::_thesis: T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
thus T -level (n + 1) c= union { (succ w) where w is Element of T : len w = n } :: according to XBOOLE_0:def_10 ::_thesis: union { (succ w) where w is Element of T : len w = n } c= T -level (n + 1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T -level (n + 1) or x in union { (succ w) where w is Element of T : len w = n } )
assume A1: x in T -level (n + 1) ; ::_thesis: x in union { (succ w) where w is Element of T : len w = n }
then reconsider t = x as Element of T ;
t | (Seg n) is FinSequence of NAT by FINSEQ_1:18;
then consider s being FinSequence of NAT such that
A2: s = t | (Seg n) ;
s is_a_prefix_of t by A2, TREES_1:def_1;
then reconsider s = s as Element of T by TREES_1:20;
A3: ex w9 being Element of T st
( t = w9 & len w9 = n + 1 ) by A1;
n + 0 <= n + 1 by XREAL_1:6;
then len s = n by A3, A2, FINSEQ_1:17;
then A4: succ s in { (succ w) where w is Element of T : len w = n } ;
Seg (n + 1) = dom t by A3, FINSEQ_1:def_3;
then t = t | (Seg (n + 1)) by RELAT_1:69;
then ex m being Element of NAT st t = s ^ <*m*> by A3, A2, Th33;
then t in succ s ;
hence x in union { (succ w) where w is Element of T : len w = n } by A4, TARSKI:def_4; ::_thesis: verum
end;
thus union { (succ w) where w is Element of T : len w = n } c= T -level (n + 1) ::_thesis: verum
proof
set X = { (succ w) where w is Element of T : len w = n } ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (succ w) where w is Element of T : len w = n } or x in T -level (n + 1) )
assume x in union { (succ w) where w is Element of T : len w = n } ; ::_thesis: x in T -level (n + 1)
then consider Y being set such that
A5: x in Y and
A6: Y in { (succ w) where w is Element of T : len w = n } by TARSKI:def_4;
consider w being Element of T such that
A7: Y = succ w and
A8: len w = n by A6;
reconsider t = x as Element of T by A5, A7;
consider k being Element of NAT such that
A9: t = w ^ <*k*> and
w ^ <*k*> in T by A5, A7;
len <*k*> = 1 by FINSEQ_1:40;
then len t = n + 1 by A8, A9, FINSEQ_1:22;
hence x in T -level (n + 1) ; ::_thesis: verum
end;
end;
theorem Th46: :: TREES_9:46
for T being finite-branching Tree
for n being Element of NAT holds T -level n is finite
proof
let T be finite-branching Tree; ::_thesis: for n being Element of NAT holds T -level n is finite
defpred S1[ Element of NAT ] means T -level $1 is finite ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: T -level n is finite ; ::_thesis: S1[n + 1]
set X = { (succ w) where w is Element of T : len w = n } ;
A3: { (succ w) where w is Element of T : len w = n } is finite
proof
defpred S2[ set , set ] means ex w being Element of T st
( $1 = w & $2 = succ w );
A4: for x being set st x in T -level n holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in T -level n implies ex y being set st S2[x,y] )
assume x in T -level n ; ::_thesis: ex y being set st S2[x,y]
then consider w being Element of T such that
A5: w = x ;
consider y being set such that
A6: y = succ w ;
take y ; ::_thesis: S2[x,y]
take w ; ::_thesis: ( x = w & y = succ w )
thus ( x = w & y = succ w ) by A5, A6; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = T -level n & ( for x being set st x in T -level n holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A4);
A8: { (succ w) where w is Element of T : len w = n } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (succ w) where w is Element of T : len w = n } or x in rng f )
assume x in { (succ w) where w is Element of T : len w = n } ; ::_thesis: x in rng f
then consider w being Element of T such that
A9: x = succ w and
A10: len w = n ;
A11: w in T -level n by A10;
then ex w9 being Element of T st
( w = w9 & f . w = succ w9 ) by A7;
hence x in rng f by A7, A9, A11, FUNCT_1:def_3; ::_thesis: verum
end;
card (rng f) c= card (dom f) by CARD_1:12;
then rng f is finite by A2, A7;
hence { (succ w) where w is Element of T : len w = n } is finite by A8; ::_thesis: verum
end;
A12: for Y being set st Y in { (succ w) where w is Element of T : len w = n } holds
Y is finite
proof
let Y be set ; ::_thesis: ( Y in { (succ w) where w is Element of T : len w = n } implies Y is finite )
assume Y in { (succ w) where w is Element of T : len w = n } ; ::_thesis: Y is finite
then ex w being Element of T st
( Y = succ w & len w = n ) ;
hence Y is finite ; ::_thesis: verum
end;
T -level (n + 1) = union { (succ w) where w is Element of T : len w = n } by Th45;
hence S1[n + 1] by A3, A12, FINSET_1:7; ::_thesis: verum
end;
A13: S1[ 0 ] by Th44;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1); ::_thesis: verum
end;
theorem Th47: :: TREES_9:47
for T being finite-branching Tree holds
( T is finite iff ex n being Element of NAT st T -level n = {} )
proof
let T be finite-branching Tree; ::_thesis: ( T is finite iff ex n being Element of NAT st T -level n = {} )
deffunc H1( Element of NAT ) -> Level of T = T -level $1;
now__::_thesis:_(_T_is_finite_implies_ex_n_being_Element_of_NAT_st_T_-level_n_=_{}_)
assume A1: T is finite ; ::_thesis: ex n being Element of NAT st T -level n = {}
now__::_thesis:_ex_n_being_Element_of_NAT_st_T_-level_n_=_{}
assume A2: for n being Element of NAT holds not T -level n = {} ; ::_thesis: contradiction
A3: for n being Element of NAT ex C being finite Chain of T st card C = n
proof
let n be Element of NAT ; ::_thesis: ex C being finite Chain of T st card C = n
T -level n <> {} by A2;
then consider t being set such that
A4: t in T -level n by XBOOLE_0:def_1;
consider w being Element of T such that
t = w and
A5: len w = n by A4;
ProperPrefixes w is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A6: C = ProperPrefixes w ;
card C = n by A5, A6, TREES_1:35;
hence ex C being finite Chain of T st card C = n ; ::_thesis: verum
end;
for t being Element of T holds succ t is finite ;
then not for C being Chain of T holds C is finite by A3, TREES_2:29;
hence contradiction by A1; ::_thesis: verum
end;
hence ex n being Element of NAT st T -level n = {} ; ::_thesis: verum
end;
hence ( T is finite implies ex n being Element of NAT st T -level n = {} ) ; ::_thesis: ( ex n being Element of NAT st T -level n = {} implies T is finite )
given n being Element of NAT such that A7: T -level n = {} ; ::_thesis: T is finite
set X = { H1(m) where m is Element of NAT : m <= n } ;
A8: T c= union { H1(m) where m is Element of NAT : m <= n }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in union { H1(m) where m is Element of NAT : m <= n } )
assume x in T ; ::_thesis: x in union { H1(m) where m is Element of NAT : m <= n }
then reconsider t = x as Element of T ;
consider m being Element of NAT such that
A9: m = len t ;
A10: t in H1(m) by A9;
len t < n
proof
consider q being FinSequence such that
A11: q = t | (Seg n) and
A12: q is_a_prefix_of t by Th32;
assume n <= len t ; ::_thesis: contradiction
then A13: len q = n by A11, FINSEQ_1:17;
reconsider q = q as Element of T by A12, TREES_1:20;
q in T -level n by A13;
hence contradiction by A7; ::_thesis: verum
end;
then H1(m) in { H1(m) where m is Element of NAT : m <= n } by A9;
hence x in union { H1(m) where m is Element of NAT : m <= n } by A10, TARSKI:def_4; ::_thesis: verum
end;
A14: { H1(m) where m is Element of NAT : m <= n } is finite
proof
defpred S1[ set , set ] means ex l, m being Element of NAT st
( m = l + 1 & $1 = m & H1(l) = $2 );
A15: for k being Nat st k in Seg (n + 1) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (n + 1) implies ex x being set st S1[k,x] )
assume k in Seg (n + 1) ; ::_thesis: ex x being set st S1[k,x]
then 0 <> k by FINSEQ_1:1;
then consider l being Nat such that
A16: k = l + 1 by NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
consider x being set such that
A17: x = H1(l) ;
take x ; ::_thesis: S1[k,x]
take l ; ::_thesis: ex m being Element of NAT st
( m = l + 1 & k = m & H1(l) = x )
take l + 1 ; ::_thesis: ( l + 1 = l + 1 & k = l + 1 & H1(l) = x )
thus ( l + 1 = l + 1 & k = l + 1 & H1(l) = x ) by A16, A17; ::_thesis: verum
end;
consider p being FinSequence such that
A18: ( dom p = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A15);
A19: for k being Element of NAT st k + 1 in Seg (n + 1) holds
p . (k + 1) = H1(k)
proof
let k be Element of NAT ; ::_thesis: ( k + 1 in Seg (n + 1) implies p . (k + 1) = H1(k) )
assume k + 1 in Seg (n + 1) ; ::_thesis: p . (k + 1) = H1(k)
then ex l, m being Element of NAT st
( m = l + 1 & k + 1 = m & H1(l) = p . (k + 1) ) by A18;
hence p . (k + 1) = H1(k) ; ::_thesis: verum
end;
{ H1(m) where m is Element of NAT : m <= n } c= rng p
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { H1(m) where m is Element of NAT : m <= n } or y in rng p )
assume y in { H1(m) where m is Element of NAT : m <= n } ; ::_thesis: y in rng p
then consider m being Element of NAT such that
A20: y = H1(m) and
A21: m <= n ;
0 <= m by NAT_1:2;
then A22: 0 + 1 <= m + 1 by XREAL_1:6;
m + 1 <= n + 1 by A21, XREAL_1:6;
then A23: m + 1 in Seg (n + 1) by A22, FINSEQ_1:1;
then p . (m + 1) = H1(m) by A19;
hence y in rng p by A18, A20, A23, FUNCT_1:def_3; ::_thesis: verum
end;
hence { H1(m) where m is Element of NAT : m <= n } is finite ; ::_thesis: verum
end;
for Y being set st Y in { H1(m) where m is Element of NAT : m <= n } holds
Y is finite
proof
let Y be set ; ::_thesis: ( Y in { H1(m) where m is Element of NAT : m <= n } implies Y is finite )
assume Y in { H1(m) where m is Element of NAT : m <= n } ; ::_thesis: Y is finite
then ex m being Element of NAT st
( Y = H1(m) & m <= n ) ;
hence Y is finite by Th46; ::_thesis: verum
end;
then union { H1(m) where m is Element of NAT : m <= n } is finite by A14, FINSET_1:7;
hence T is finite by A8; ::_thesis: verum
end;
theorem Th48: :: TREES_9:48
for T being finite-branching Tree st not T is finite holds
ex C being Chain of T st not C is finite
proof
let T be finite-branching Tree; ::_thesis: ( not T is finite implies ex C being Chain of T st not C is finite )
assume A1: not T is finite ; ::_thesis: not for C being Chain of T holds C is finite
A2: for n being Element of NAT ex C being finite Chain of T st card C = n
proof
let n be Element of NAT ; ::_thesis: ex C being finite Chain of T st card C = n
T -level n <> {} by A1, Th47;
then consider t being set such that
A3: t in T -level n by XBOOLE_0:def_1;
A4: ex w being Element of T st
( t = w & len w = n ) by A3;
reconsider t = t as Element of T by A3;
ProperPrefixes t is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A5: C = ProperPrefixes t ;
card C = n by A4, A5, TREES_1:35;
hence ex C being finite Chain of T st card C = n ; ::_thesis: verum
end;
for t being Element of T holds succ t is finite ;
hence not for C being Chain of T holds C is finite by A2, TREES_2:29; ::_thesis: verum
end;
theorem Th49: :: TREES_9:49
for T being finite-branching Tree st not T is finite holds
ex B being Branch of T st not B is finite
proof
let T be finite-branching Tree; ::_thesis: ( not T is finite implies ex B being Branch of T st not B is finite )
assume not T is finite ; ::_thesis: not for B being Branch of T holds B is finite
then consider C being Chain of T such that
A1: not C is finite by Th48;
consider B being Branch of T such that
A2: C c= B by TREES_2:28;
not B is finite by A1, A2;
hence not for B being Branch of T holds B is finite ; ::_thesis: verum
end;
theorem Th50: :: TREES_9:50
for T being Tree
for C being Chain of T
for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
proof
let T be Tree; ::_thesis: for C being Chain of T
for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
let C be Chain of T; ::_thesis: for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
let t be Element of T; ::_thesis: ( t in C & not C is finite implies ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 ) )
assume that
A1: t in C and
A2: not C is finite ; ::_thesis: ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
now__::_thesis:_ex_t9_being_Element_of_T_st_
(_t9_in_C_&_t_is_a_proper_prefix_of_t9_)
assume A3: for t9 being Element of T holds
( not t9 in C or not t is_a_proper_prefix_of t9 ) ; ::_thesis: contradiction
A4: for t9 being Element of T st t9 in C holds
t9 is_a_prefix_of t
proof
let t9 be Element of T; ::_thesis: ( t9 in C implies t9 is_a_prefix_of t )
assume A5: t9 in C ; ::_thesis: t9 is_a_prefix_of t
now__::_thesis:_t9_is_a_prefix_of_t
assume A6: not t9 is_a_prefix_of t ; ::_thesis: contradiction
t,t9 are_c=-comparable by A1, A5, TREES_2:def_3;
then t is_a_prefix_of t9 by A6, XBOOLE_0:def_9;
then t is_a_proper_prefix_of t9 by A6, XBOOLE_0:def_8;
hence contradiction by A3, A5; ::_thesis: verum
end;
hence t9 is_a_prefix_of t ; ::_thesis: verum
end;
C c= (ProperPrefixes t) \/ {t}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in (ProperPrefixes t) \/ {t} )
assume A7: x in C ; ::_thesis: x in (ProperPrefixes t) \/ {t}
then reconsider t9 = x as Element of T ;
A8: t9 is_a_prefix_of t by A4, A7;
t9 in (ProperPrefixes t) \/ {t}
proof
percases ( t9 is_a_proper_prefix_of t or t9 = t ) by A8, XBOOLE_0:def_8;
suppose t9 is_a_proper_prefix_of t ; ::_thesis: t9 in (ProperPrefixes t) \/ {t}
then t9 in ProperPrefixes t by TREES_1:12;
hence t9 in (ProperPrefixes t) \/ {t} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose t9 = t ; ::_thesis: t9 in (ProperPrefixes t) \/ {t}
then t9 in {t} by TARSKI:def_1;
hence t9 in (ProperPrefixes t) \/ {t} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence x in (ProperPrefixes t) \/ {t} ; ::_thesis: verum
end;
hence contradiction by A2; ::_thesis: verum
end;
hence ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 ) ; ::_thesis: verum
end;
theorem Th51: :: TREES_9:51
for T being Tree
for B being Branch of T
for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )
proof
let T be Tree; ::_thesis: for B being Branch of T
for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )
let B be Branch of T; ::_thesis: for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )
let t be Element of T; ::_thesis: ( t in B & not B is finite implies ex t9 being Element of T st
( t9 in B & t9 in succ t ) )
assume ( t in B & not B is finite ) ; ::_thesis: ex t9 being Element of T st
( t9 in B & t9 in succ t )
then consider t99 being Element of T such that
A1: t99 in B and
A2: t is_a_proper_prefix_of t99 by Th50;
t is_a_prefix_of t99 by A2, XBOOLE_0:def_8;
then consider r being FinSequence such that
A3: t99 = t ^ r by TREES_1:1;
reconsider r = r as FinSequence of NAT by A3, FINSEQ_1:36;
r | (Seg 1) is FinSequence of NAT by FINSEQ_1:18;
then consider r1 being FinSequence of NAT such that
A4: r1 = r | (Seg 1) ;
1 <= len r
proof
len t < len t99 by A2, TREES_1:6;
then consider m being Nat such that
A5: (len t) + m = len t99 by NAT_1:10;
m <> 0 by A2, A5, TREES_1:6;
then 0 < m by NAT_1:3;
then A6: 0 + 1 <= m by NAT_1:13;
len t99 = (len t) + (len r) by A3, FINSEQ_1:22;
hence 1 <= len r by A5, A6; ::_thesis: verum
end;
then consider n being Element of NAT such that
A7: r1 = <*n*> by A4, Th34;
A8: r1 is_a_prefix_of r by A4, TREES_1:def_1;
then A9: t ^ r1 is_a_prefix_of t99 by A3, FINSEQ_6:13;
t ^ <*n*> in T by A3, A7, A8, FINSEQ_6:13, TREES_1:20;
then consider t9 being Element of T such that
A10: t9 = t ^ <*n*> ;
t9 in succ t by A10;
hence ex t9 being Element of T st
( t9 in B & t9 in succ t ) by A1, A7, A9, A10, TREES_2:25; ::_thesis: verum
end;
theorem Th52: :: TREES_9:52
for f being Function of NAT,NAT st ( for n being Element of NAT holds f . (n + 1) <= f . n ) holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m
proof
let f be Function of NAT,NAT; ::_thesis: ( ( for n being Element of NAT holds f . (n + 1) <= f . n ) implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m )
assume A1: for n being Element of NAT holds f . (n + 1) <= f . n ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m
A2: for m, k being Element of NAT st m <= k holds
f . k <= f . m
proof
defpred S1[ Element of NAT ] means for m being Element of NAT st m <= $1 holds
f . $1 <= f . m;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_m_being_Element_of_NAT_st_m_<=_k_+_1_holds_
f_._(k_+_1)_<=_f_._m
let m be Element of NAT ; ::_thesis: ( m <= k + 1 implies f . (k + 1) <= f . b1 )
assume A5: m <= k + 1 ; ::_thesis: f . (k + 1) <= f . b1
percases ( m <= k or m = k + 1 ) by A5, NAT_1:8;
supposeA6: m <= k ; ::_thesis: f . (k + 1) <= f . b1
reconsider fk = f . k, fm = f . m, fk1 = f . (k + 1) as Element of NAT ;
A7: fk1 <= fk by A1;
fk <= fm by A4, A6;
hence f . (k + 1) <= f . m by A7, XXREAL_0:2; ::_thesis: verum
end;
suppose m = k + 1 ; ::_thesis: f . (k + 1) <= f . b1
hence f . (k + 1) <= f . m ; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A8: S1[ 0 ]
proof
let m be Element of NAT ; ::_thesis: ( m <= 0 implies f . 0 <= f . m )
assume A9: m <= 0 ; ::_thesis: f . 0 <= f . m
0 <= m by NAT_1:2;
hence f . 0 <= f . m by A9, XXREAL_0:1; ::_thesis: verum
end;
A10: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A3);
let m, k be Element of NAT ; ::_thesis: ( m <= k implies f . k <= f . m )
assume m <= k ; ::_thesis: f . k <= f . m
hence f . k <= f . m by A10; ::_thesis: verum
end;
defpred S1[ set ] means $1 in rng f;
A11: ex k being Nat st S1[k]
proof
consider y being set such that
A12: y = f . 0 ;
reconsider k = y as Element of NAT by A12;
take k ; ::_thesis: S1[k]
dom f = NAT by FUNCT_2:def_1;
hence S1[k] by A12, FUNCT_1:def_3; ::_thesis: verum
end;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A11);
then consider l being Nat such that
A13: l in rng f and
A14: for n being Nat st n in rng f holds
l <= n ;
consider x being set such that
A15: x in dom f and
A16: l = f . x by A13, FUNCT_1:def_3;
reconsider m = x as Element of NAT by A15;
A17: dom f = NAT by FUNCT_2:def_1;
for k being Element of NAT st m <= k holds
f . k = f . m
proof
let k be Element of NAT ; ::_thesis: ( m <= k implies f . k = f . m )
assume A18: m <= k ; ::_thesis: f . k = f . m
now__::_thesis:_not_f_._k_<>_f_._m
reconsider fk = f . k, fm = f . m as Element of NAT ;
assume A19: f . k <> f . m ; ::_thesis: contradiction
fk <= fm by A2, A18;
then A20: fk < fm by A19, XXREAL_0:1;
f . k in rng f by A17, FUNCT_1:def_3;
hence contradiction by A14, A16, A20; ::_thesis: verum
end;
hence f . k = f . m ; ::_thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m ; ::_thesis: verum
end;
scheme :: TREES_9:sch 3
FinDecTree{ F1() -> non empty set , F2() -> finite-branching DecoratedTree of F1(), F3( Element of F1()) -> Element of NAT } :
F2() is finite
provided
A1: for t, t9 being Element of dom F2()
for d being Element of F1() st t9 in succ t & d = F2() . t9 holds
F3(d) < F3((F2() . t))
proof
now__::_thesis:_F2()_is_finite
assume not F2() is finite ; ::_thesis: contradiction
then not dom F2() is finite by FINSET_1:10;
then consider B being Branch of dom F2() such that
A2: not B is finite by Th49;
defpred S1[ set , set ] means ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & $1 = F2() . t & $2 = F2() . t9 );
defpred S2[ set ] means ex t being Element of dom F2() st
( t in B & $1 = F2() . t );
A3: for x being set st x in F1() & S2[x] holds
ex y being set st
( y in F1() & S1[x,y] & S2[y] )
proof
let x be set ; ::_thesis: ( x in F1() & S2[x] implies ex y being set st
( y in F1() & S1[x,y] & S2[y] ) )
assume that
x in F1() and
A4: S2[x] ; ::_thesis: ex y being set st
( y in F1() & S1[x,y] & S2[y] )
consider t being Element of dom F2() such that
A5: t in B and
A6: x = F2() . t by A4;
consider t9 being Element of dom F2() such that
A7: ( t9 in B & t9 in succ t ) by A2, A5, Th51;
ex y being set st y = F2() . t9 ;
hence ex y being set st
( y in F1() & S1[x,y] & S2[y] ) by A5, A6, A7; ::_thesis: verum
end;
{} in B by TREES_2:26;
then S2[F2() . {}] ;
then A8: ( F2() . {} in F1() & S2[F2() . {}] ) ;
ex g being Function st
( dom g = NAT & rng g c= F1() & g . 0 = F2() . {} & ( for k being Element of NAT holds
( S1[g . k,g . (k + 1)] & S2[g . k] ) ) ) from TREES_2:sch_5(A8, A3);
then consider g being Function such that
dom g = NAT and
rng g c= F1() and
g . 0 = F2() . {} and
A9: for k being Element of NAT holds
( ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & g . k = F2() . t & g . (k + 1) = F2() . t9 ) & ex t being Element of dom F2() st
( t in B & g . k = F2() . t ) ) ;
defpred S3[ set , set ] means ex d being Element of F1() st
( d = g . $1 & $2 = F3(d) );
A10: for x being set st x in NAT holds
ex y being set st
( y in NAT & S3[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in NAT & S3[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in NAT & S3[x,y] )
then reconsider k = x as Element of NAT ;
consider t being Element of dom F2() such that
t in B and
A11: g . k = F2() . t by A9;
ex y being set st y = F3((F2() . t)) ;
hence ex y being set st
( y in NAT & S3[x,y] ) by A11; ::_thesis: verum
end;
ex f being Function of NAT,NAT st
for x being set st x in NAT holds
S3[x,f . x] from FUNCT_2:sch_1(A10);
then consider f being Function of NAT,NAT such that
A12: for x being set st x in NAT holds
ex d being Element of F1() st
( d = g . x & f . x = F3(d) ) ;
A13: for k being Element of NAT ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) )
proof
let k be Element of NAT ; ::_thesis: ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) )
A14: ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & g . k = F2() . t & g . (k + 1) = F2() . t9 ) by A9;
( ex d being Element of F1() st
( d = g . k & f . k = F3(d) ) & ex d1 being Element of F1() st
( d1 = g . (k + 1) & f . (k + 1) = F3(d1) ) ) by A12;
hence ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) ) by A14; ::_thesis: verum
end;
A15: for n being Element of NAT ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n )
proof
let n be Element of NAT ; ::_thesis: ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n )
ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) ) by A13;
hence ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n ) by A1; ::_thesis: verum
end;
for n being Element of NAT holds f . (n + 1) <= f . n
proof
let n be Element of NAT ; ::_thesis: f . (n + 1) <= f . n
ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n ) by A15;
hence f . (n + 1) <= f . n ; ::_thesis: verum
end;
then consider m being Element of NAT such that
A16: for n being Element of NAT st m <= n holds
f . n = f . m by Th52;
A17: m + 0 <= m + 1 by XREAL_1:6;
ex t, t9 being Element of dom F2() st
( t9 in succ t & f . m = F3((F2() . t)) & f . (m + 1) = F3((F2() . t9)) & f . (m + 1) < f . m ) by A15;
hence contradiction by A16, A17; ::_thesis: verum
end;
hence F2() is finite ; ::_thesis: verum
end;