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