:: TREES_2 semantic presentation begin theorem Th1: :: TREES_2:1 for v1, v2, v being FinSequence st v1 is_a_prefix_of v & v2 is_a_prefix_of v holds v1,v2 are_c=-comparable proof let p, q, r be FinSequence; ::_thesis: ( p is_a_prefix_of r & q is_a_prefix_of r implies p,q are_c=-comparable ) assume p is_a_prefix_of r ; ::_thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable ) then A1: ex p9 being FinSequence st r = p ^ p9 by TREES_1:1; assume q is_a_prefix_of r ; ::_thesis: p,q are_c=-comparable then A2: ex q9 being FinSequence st r = q ^ q9 by TREES_1:1; ( len p <= len q or len q <= len p ) ; then ( ex t being FinSequence st p ^ t = q or ex t being FinSequence st q ^ t = p ) by A1, A2, FINSEQ_1:47; hence ( p is_a_prefix_of q or q is_a_prefix_of p ) by TREES_1:1; :: according to XBOOLE_0:def_9 ::_thesis: verum end; theorem Th2: :: TREES_2:2 for v1, v2, v being FinSequence st v1 is_a_proper_prefix_of v & v2 is_a_prefix_of v holds v1,v2 are_c=-comparable proof let p, q, r be FinSequence; ::_thesis: ( p is_a_proper_prefix_of r & q is_a_prefix_of r implies p,q are_c=-comparable ) assume p is_a_proper_prefix_of r ; ::_thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable ) then p is_a_prefix_of r by XBOOLE_0:def_8; hence ( not q is_a_prefix_of r or p,q are_c=-comparable ) by Th1; ::_thesis: verum end; theorem Th3: :: TREES_2:3 for k being Element of NAT for v1 being FinSequence st len v1 = k + 1 holds ex v2 being FinSequence ex x being set st ( v1 = v2 ^ <*x*> & len v2 = k ) proof let k be Element of NAT ; ::_thesis: for v1 being FinSequence st len v1 = k + 1 holds ex v2 being FinSequence ex x being set st ( v1 = v2 ^ <*x*> & len v2 = k ) let v1 be FinSequence; ::_thesis: ( len v1 = k + 1 implies ex v2 being FinSequence ex x being set st ( v1 = v2 ^ <*x*> & len v2 = k ) ) assume A1: len v1 = k + 1 ; ::_thesis: ex v2 being FinSequence ex x being set st ( v1 = v2 ^ <*x*> & len v2 = k ) reconsider v2 = v1 | (Seg k) as FinSequence by FINSEQ_1:15; v2 is_a_prefix_of v1 by TREES_1:def_1; then consider v being FinSequence such that A2: v1 = v2 ^ v by TREES_1:1; take v2 ; ::_thesis: ex x being set st ( v1 = v2 ^ <*x*> & len v2 = k ) take v . 1 ; ::_thesis: ( v1 = v2 ^ <*(v . 1)*> & len v2 = k ) A3: k <= k + 1 by NAT_1:11; then len v2 = k by A1, FINSEQ_1:17; then k + (len v) = k + 1 by A1, A2, FINSEQ_1:22; hence ( v1 = v2 ^ <*(v . 1)*> & len v2 = k ) by A1, A2, A3, FINSEQ_1:17, FINSEQ_1:40; ::_thesis: verum end; theorem Th4: :: TREES_2:4 for x being set for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v} proof let x be set ; ::_thesis: for v being FinSequence holds ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v} let v be FinSequence; ::_thesis: ProperPrefixes (v ^ <*x*>) = (ProperPrefixes v) \/ {v} thus ProperPrefixes (v ^ <*x*>) c= (ProperPrefixes v) \/ {v} :: according to XBOOLE_0:def_10 ::_thesis: (ProperPrefixes v) \/ {v} c= ProperPrefixes (v ^ <*x*>) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ProperPrefixes (v ^ <*x*>) or y in (ProperPrefixes v) \/ {v} ) assume y in ProperPrefixes (v ^ <*x*>) ; ::_thesis: y in (ProperPrefixes v) \/ {v} then consider v1 being FinSequence such that A1: y = v1 and A2: v1 is_a_proper_prefix_of v ^ <*x*> by TREES_1:def_2; ( ( v1 is_a_prefix_of v & v1 <> v ) or v1 = v ) by A2, TREES_1:9; then ( v1 is_a_proper_prefix_of v or v1 in {v} ) by TARSKI:def_1, XBOOLE_0:def_8; then ( y in ProperPrefixes v or y in {v} ) by A1, TREES_1:def_2; hence y in (ProperPrefixes v) \/ {v} by XBOOLE_0:def_3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (ProperPrefixes v) \/ {v} or y in ProperPrefixes (v ^ <*x*>) ) assume y in (ProperPrefixes v) \/ {v} ; ::_thesis: y in ProperPrefixes (v ^ <*x*>) then A3: ( y in ProperPrefixes v or y in {v} ) by XBOOLE_0:def_3; A4: now__::_thesis:_(_y_in_ProperPrefixes_v_implies_y_in_ProperPrefixes_(v_^_<*x*>)_) assume y in ProperPrefixes v ; ::_thesis: y in ProperPrefixes (v ^ <*x*>) then consider v1 being FinSequence such that A5: y = v1 and A6: v1 is_a_proper_prefix_of v by TREES_1:def_2; v is_a_prefix_of v ^ <*x*> by TREES_1:1; then v1 is_a_proper_prefix_of v ^ <*x*> by A6, XBOOLE_1:58; hence y in ProperPrefixes (v ^ <*x*>) by A5, TREES_1:def_2; ::_thesis: verum end; v ^ {} = v by FINSEQ_1:34; then ( v is_a_prefix_of v ^ <*x*> & v <> v ^ <*x*> ) by FINSEQ_1:33, TREES_1:1; then v is_a_proper_prefix_of v ^ <*x*> by XBOOLE_0:def_8; then ( y in ProperPrefixes v or ( y = v & v in ProperPrefixes (v ^ <*x*>) ) ) by A3, TARSKI:def_1, TREES_1:def_2; hence y in ProperPrefixes (v ^ <*x*>) by A4; ::_thesis: verum end; scheme :: TREES_2:sch 1 TreeStructInd{ F1() -> Tree, P1[ set ] } : for t being Element of F1() holds P1[t] provided A1: P1[ {} ] and A2: for t being Element of F1() for n being Element of NAT st P1[t] & t ^ <*n*> in F1() holds P1[t ^ <*n*>] proof defpred S1[ set ] means for t being Element of F1() st len t = $1 holds P1[t]; for x being set st card x = 0 holds x = {} ; then A3: S1[ 0 ] by A1; A4: 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 A5: for t being Element of F1() st len t = k holds P1[t] ; ::_thesis: S1[k + 1] let t be Element of F1(); ::_thesis: ( len t = k + 1 implies P1[t] ) assume len t = k + 1 ; ::_thesis: P1[t] then consider v being FinSequence, x being set such that A6: t = v ^ <*x*> and A7: len v = k by Th3; reconsider v = v as FinSequence of NAT by A6, FINSEQ_1:36; reconsider v = v as Element of F1() by A6, TREES_1:21; rng <*x*> c= rng t by A6, FINSEQ_1:30; then ( rng <*x*> = {x} & rng <*x*> c= NAT ) by FINSEQ_1:39, XBOOLE_1:1; then reconsider x = x as Element of NAT by ZFMISC_1:31; A8: P1[v] by A5, A7; x = x ; hence P1[t] by A2, A6, A8; ::_thesis: verum end; A9: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A4); let t be Element of F1(); ::_thesis: P1[t] len t = len t ; hence P1[t] by A9; ::_thesis: verum end; theorem Th5: :: TREES_2:5 for W1, W2 being Tree st ( for p being FinSequence of NAT holds ( p in W1 iff p in W2 ) ) holds W1 = W2 proof let W1, W2 be Tree; ::_thesis: ( ( for p being FinSequence of NAT holds ( p in W1 iff p in W2 ) ) implies W1 = W2 ) assume A1: for p being FinSequence of NAT holds ( p in W1 iff p in W2 ) ; ::_thesis: W1 = W2 thus W1 c= W2 :: according to XBOOLE_0:def_10 ::_thesis: W2 c= W1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W1 or x in W2 ) assume x in W1 ; ::_thesis: x in W2 then reconsider p = x as Element of W1 ; p in W2 by A1; hence x in W2 ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W2 or x in W1 ) assume x in W2 ; ::_thesis: x in W1 then reconsider p = x as Element of W2 ; p in W1 by A1; hence x in W1 ; ::_thesis: verum end; definition let W1, W2 be Tree; redefine pred W1 = W2 means :: TREES_2:def 1 for p being FinSequence of NAT holds ( p in W1 iff p in W2 ); compatibility ( W1 = W2 iff for p being FinSequence of NAT holds ( p in W1 iff p in W2 ) ) by Th5; end; :: deftheorem defines = TREES_2:def_1_:_ for W1, W2 being Tree holds ( W1 = W2 iff for p being FinSequence of NAT holds ( p in W1 iff p in W2 ) ); theorem :: TREES_2:6 for W being Tree for p being FinSequence of NAT st p in W holds W = W with-replacement (p,(W | p)) proof let W be Tree; ::_thesis: for p being FinSequence of NAT st p in W holds W = W with-replacement (p,(W | p)) let p be FinSequence of NAT ; ::_thesis: ( p in W implies W = W with-replacement (p,(W | p)) ) assume A1: p in W ; ::_thesis: W = W with-replacement (p,(W | p)) now__::_thesis:_for_q_being_FinSequence_of_NAT_holds_ (_(_q_in_W_implies_q_in_W_with-replacement_(p,(W_|_p))_)_&_(_q_in_W_with-replacement_(p,(W_|_p))_implies_q_in_W_)_) let q be FinSequence of NAT ; ::_thesis: ( ( q in W implies q in W with-replacement (p,(W | p)) ) & ( q in W with-replacement (p,(W | p)) implies q in W ) ) thus ( q in W implies q in W with-replacement (p,(W | p)) ) ::_thesis: ( q in W with-replacement (p,(W | p)) implies q in W ) proof assume A2: q in W ; ::_thesis: q in W with-replacement (p,(W | p)) now__::_thesis:_(_p_is_a_proper_prefix_of_q_implies_ex_r_being_FinSequence_of_NAT_st_ (_r_in_W_|_p_&_q_=_p_^_r_)_) assume p is_a_proper_prefix_of q ; ::_thesis: ex r being FinSequence of NAT st ( r in W | p & q = p ^ r ) then p is_a_prefix_of q by XBOOLE_0:def_8; then consider r being FinSequence such that A3: q = p ^ r by TREES_1:1; rng r c= rng q by A3, FINSEQ_1:30; then rng r c= NAT by XBOOLE_1:1; then reconsider r = r as FinSequence of NAT by FINSEQ_1:def_4; take r = r; ::_thesis: ( r in W | p & q = p ^ r ) thus ( r in W | p & q = p ^ r ) by A1, A2, A3, TREES_1:def_6; ::_thesis: verum end; hence q in W with-replacement (p,(W | p)) by A1, A2, TREES_1:def_9; ::_thesis: verum end; assume that A4: q in W with-replacement (p,(W | p)) and A5: not q in W ; ::_thesis: contradiction ex r being FinSequence of NAT st ( r in W | p & q = p ^ r ) by A1, A4, A5, TREES_1:def_9; hence contradiction by A1, A5, TREES_1:def_6; ::_thesis: verum end; hence W = W with-replacement (p,(W | p)) by Th5; ::_thesis: verum end; theorem Th7: :: TREES_2:7 for W, W1 being Tree for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds q in W with-replacement (p,W1) proof let W, W1 be Tree; ::_thesis: for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds q in W with-replacement (p,W1) let p, q be FinSequence of NAT ; ::_thesis: ( p in W & q in W & not p is_a_prefix_of q implies q in W with-replacement (p,W1) ) ( not p is_a_prefix_of q implies not p is_a_proper_prefix_of q ) by XBOOLE_0:def_8; hence ( p in W & q in W & not p is_a_prefix_of q implies q in W with-replacement (p,W1) ) by TREES_1:def_9; ::_thesis: verum end; theorem :: TREES_2:8 for W, W1, W2 being Tree for p, q being FinSequence of NAT st p in W & q in W & not p,q are_c=-comparable holds (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1) proof let W, W1, W2 be Tree; ::_thesis: for p, q being FinSequence of NAT st p in W & q in W & not p,q are_c=-comparable holds (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1) let p, q be FinSequence of NAT ; ::_thesis: ( p in W & q in W & not p,q are_c=-comparable implies (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1) ) assume that A1: p in W and A2: q in W and A3: not p,q are_c=-comparable ; ::_thesis: (W with-replacement (p,W1)) with-replacement (q,W2) = (W with-replacement (q,W2)) with-replacement (p,W1) A4: not p is_a_prefix_of q by A3, XBOOLE_0:def_9; not q is_a_prefix_of p by A3, XBOOLE_0:def_9; then A5: p in W with-replacement (q,W2) by A1, A2, Th7; A6: q in W with-replacement (p,W1) by A1, A2, A4, Th7; let r be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( r in (W with-replacement (p,W1)) with-replacement (q,W2) iff r in (W with-replacement (q,W2)) with-replacement (p,W1) ) thus ( r in (W with-replacement (p,W1)) with-replacement (q,W2) implies r in (W with-replacement (q,W2)) with-replacement (p,W1) ) ::_thesis: ( r in (W with-replacement (q,W2)) with-replacement (p,W1) implies r in (W with-replacement (p,W1)) with-replacement (q,W2) ) proof assume r in (W with-replacement (p,W1)) with-replacement (q,W2) ; ::_thesis: r in (W with-replacement (q,W2)) with-replacement (p,W1) then ( ( r in W with-replacement (p,W1) & not q is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st ( r1 in W2 & r = q ^ r1 ) ) by A6, TREES_1:def_9; then ( ( r in W & not p is_a_proper_prefix_of r & not q is_a_proper_prefix_of r ) or ( ex r2 being FinSequence of NAT st ( r2 in W1 & r = p ^ r2 ) & not q is_a_proper_prefix_of r ) or ( q is_a_prefix_of r & ex r1 being FinSequence of NAT st ( r1 in W2 & r = q ^ r1 ) ) ) by A1, TREES_1:1, TREES_1:def_9; then ( ( r in W with-replacement (q,W2) & not p is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st ( r1 in W1 & r = p ^ r1 ) ) by A2, A3, Th2, TREES_1:def_9; hence r in (W with-replacement (q,W2)) with-replacement (p,W1) by A5, TREES_1:def_9; ::_thesis: verum end; assume r in (W with-replacement (q,W2)) with-replacement (p,W1) ; ::_thesis: r in (W with-replacement (p,W1)) with-replacement (q,W2) then ( ( r in W with-replacement (q,W2) & not p is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st ( r1 in W1 & r = p ^ r1 ) ) by A5, TREES_1:def_9; then ( ( r in W & not q is_a_proper_prefix_of r & not p is_a_proper_prefix_of r ) or ( ex r2 being FinSequence of NAT st ( r2 in W2 & r = q ^ r2 ) & not p is_a_proper_prefix_of r ) or ( p is_a_prefix_of r & ex r1 being FinSequence of NAT st ( r1 in W1 & r = p ^ r1 ) ) ) by A2, TREES_1:1, TREES_1:def_9; then ( ( r in W with-replacement (p,W1) & not q is_a_proper_prefix_of r ) or ex r1 being FinSequence of NAT st ( r1 in W2 & r = q ^ r1 ) ) by A1, A3, Th2, TREES_1:def_9; hence r in (W with-replacement (p,W1)) with-replacement (q,W2) by A6, TREES_1:def_9; ::_thesis: verum end; definition let IT be Tree; attrIT is finite-order means :: TREES_2:def 2 ex n being Element of NAT st for t being Element of IT holds not t ^ <*n*> in IT; end; :: deftheorem defines finite-order TREES_2:def_2_:_ for IT being Tree holds ( IT is finite-order iff ex n being Element of NAT st for t being Element of IT holds not t ^ <*n*> in IT ); registration cluster non empty Tree-like finite-order for set ; existence ex b1 being Tree st b1 is finite-order proof reconsider T = {{}} as Tree ; take T ; ::_thesis: T is finite-order take 0 ; :: according to TREES_2:def_2 ::_thesis: for t being Element of T holds not t ^ <*0*> in T let t be Element of T; ::_thesis: not t ^ <*0*> in T thus not t ^ <*0*> in T by TARSKI:def_1; ::_thesis: verum end; end; definition let W be Tree; mode Chain of W -> Subset of W means :Def3: :: TREES_2:def 3 for p, q being FinSequence of NAT st p in it & q in it holds p,q are_c=-comparable ; existence ex b1 being Subset of W st for p, q being FinSequence of NAT st p in b1 & q in b1 holds p,q are_c=-comparable proof reconsider S = {} as Subset of W by XBOOLE_1:2; take S ; ::_thesis: for p, q being FinSequence of NAT st p in S & q in S holds p,q are_c=-comparable let p, q be FinSequence of NAT ; ::_thesis: ( p in S & q in S implies p,q are_c=-comparable ) thus ( p in S & q in S implies p,q are_c=-comparable ) ; ::_thesis: verum end; mode Level of W -> Subset of W means :Def4: :: TREES_2:def 4 ex n being Nat st it = { w where w is Element of W : len w = n } ; existence ex b1 being Subset of W ex n being Nat st b1 = { w where w is Element of W : len w = n } proof {} in W by TREES_1:22; then reconsider L = {{}} as Subset of W by ZFMISC_1:31; take L ; ::_thesis: ex n being Nat st L = { w where w is Element of W : len w = n } take 0 ; ::_thesis: L = { w where w is Element of W : len w = 0 } thus L c= { w where w is Element of W : len w = 0 } :: according to XBOOLE_0:def_10 ::_thesis: { w where w is Element of W : len w = 0 } c= L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L or x in { w where w is Element of W : len w = 0 } ) assume A1: x in L ; ::_thesis: x in { w where w is Element of W : len w = 0 } then A2: x = {} by TARSKI:def_1; len {} = 0 ; hence x in { w where w is Element of W : len w = 0 } by A1, A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of W : len w = 0 } or x in L ) assume x in { w where w is Element of W : len w = 0 } ; ::_thesis: x in L then ex w being Element of W st ( x = w & len w = 0 ) ; then x = {} ; hence x in L by TARSKI:def_1; ::_thesis: verum end; let w be Element of W; func succ w -> Subset of W equals :: TREES_2:def 5 { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } ; coherence { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } is Subset of W proof { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } or x in W ) assume x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } ; ::_thesis: x in W then ex n being Element of NAT st ( x = w ^ <*n*> & w ^ <*n*> in W ) ; hence x in W ; ::_thesis: verum end; hence { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } is Subset of W ; ::_thesis: verum end; end; :: deftheorem Def3 defines Chain TREES_2:def_3_:_ for W being Tree for b2 being Subset of W holds ( b2 is Chain of W iff for p, q being FinSequence of NAT st p in b2 & q in b2 holds p,q are_c=-comparable ); :: deftheorem Def4 defines Level TREES_2:def_4_:_ for W being Tree for b2 being Subset of W holds ( b2 is Level of W iff ex n being Nat st b2 = { w where w is Element of W : len w = n } ); :: deftheorem defines succ TREES_2:def_5_:_ for W being Tree for w being Element of W holds succ w = { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } ; theorem :: TREES_2:9 for W being Tree for L being Level of W holds L is AntiChain_of_Prefixes of W proof let W be Tree; ::_thesis: for L being Level of W holds L is AntiChain_of_Prefixes of W let L be Level of W; ::_thesis: L is AntiChain_of_Prefixes of W consider n being Nat such that A1: L = { w where w is Element of W : len w = n } by Def4; L is AntiChain_of_Prefixes-like proof thus for x being set st x in L holds x is FinSequence :: according to TREES_1:def_10 ::_thesis: for b1, b2 being set holds ( not b1 in L or not b2 in L or b1 = b2 or not b1,b2 are_c=-comparable ) proof let x be set ; ::_thesis: ( x in L implies x is FinSequence ) assume x in L ; ::_thesis: x is FinSequence then x is Element of W ; hence x is FinSequence ; ::_thesis: verum end; let v1, v2 be FinSequence; ::_thesis: ( not v1 in L or not v2 in L or v1 = v2 or not v1,v2 are_c=-comparable ) assume v1 in L ; ::_thesis: ( not v2 in L or v1 = v2 or not v1,v2 are_c=-comparable ) then A2: ex w1 being Element of W st ( v1 = w1 & len w1 = n ) by A1; assume v2 in L ; ::_thesis: ( v1 = v2 or not v1,v2 are_c=-comparable ) then ex w2 being Element of W st ( v2 = w2 & len w2 = n ) by A1; hence ( v1 = v2 or not v1,v2 are_c=-comparable ) by A2, TREES_1:4; ::_thesis: verum end; hence L is AntiChain_of_Prefixes of W by TREES_1:def_11; ::_thesis: verum end; theorem :: TREES_2:10 for W being Tree for w being Element of W holds succ w is AntiChain_of_Prefixes of W proof let W be Tree; ::_thesis: for w being Element of W holds succ w is AntiChain_of_Prefixes of W let w be Element of W; ::_thesis: succ w is AntiChain_of_Prefixes of W succ w is AntiChain_of_Prefixes-like proof thus for x being set st x in succ w holds x is FinSequence :: according to TREES_1:def_10 ::_thesis: for b1, b2 being set holds ( not b1 in succ w or not b2 in succ w or b1 = b2 or not b1,b2 are_c=-comparable ) proof let x be set ; ::_thesis: ( x in succ w implies x is FinSequence ) assume x in succ w ; ::_thesis: x is FinSequence then ex i being Element of NAT st ( x = w ^ <*i*> & w ^ <*i*> in W ) ; hence x is FinSequence ; ::_thesis: verum end; let v1, v2 be FinSequence; ::_thesis: ( not v1 in succ w or not v2 in succ w or v1 = v2 or not v1,v2 are_c=-comparable ) assume v1 in succ w ; ::_thesis: ( not v2 in succ w or v1 = v2 or not v1,v2 are_c=-comparable ) then A1: ex k1 being Element of NAT st ( v1 = w ^ <*k1*> & w ^ <*k1*> in W ) ; assume v2 in succ w ; ::_thesis: ( v1 = v2 or not v1,v2 are_c=-comparable ) then A2: ex k2 being Element of NAT st ( v2 = w ^ <*k2*> & w ^ <*k2*> in W ) ; A3: len v1 = (len w) + 1 by A1, FINSEQ_2:16; len v2 = (len w) + 1 by A2, FINSEQ_2:16; hence ( v1 = v2 or not v1,v2 are_c=-comparable ) by A3, TREES_1:4; ::_thesis: verum end; hence succ w is AntiChain_of_Prefixes of W by TREES_1:def_11; ::_thesis: verum end; theorem :: TREES_2:11 for W being Tree for A being AntiChain_of_Prefixes of W for C being Chain of W ex w being Element of W st A /\ C c= {w} proof let W be Tree; ::_thesis: for A being AntiChain_of_Prefixes of W for C being Chain of W ex w being Element of W st A /\ C c= {w} let A be AntiChain_of_Prefixes of W; ::_thesis: for C being Chain of W ex w being Element of W st A /\ C c= {w} let C be Chain of W; ::_thesis: ex w being Element of W st A /\ C c= {w} A1: now__::_thesis:_for_p,_q_being_FinSequence_of_NAT_st_p_in_A_/\_C_&_q_in_A_/\_C_holds_ p_=_q let p, q be FinSequence of NAT ; ::_thesis: ( p in A /\ C & q in A /\ C implies p = q ) assume A2: ( p in A /\ C & q in A /\ C ) ; ::_thesis: p = q then A3: ( p in A & q in A ) by XBOOLE_0:def_4; ( p in C & q in C ) by A2, XBOOLE_0:def_4; then p,q are_c=-comparable by Def3; hence p = q by A3, TREES_1:def_10; ::_thesis: verum end; set w = the Element of W; now__::_thesis:_ex_w_being_Element_of_W_st_A_/\_C_c=_{w} percases ( A /\ C = {} or A /\ C <> {} ) ; suppose A /\ C = {} ; ::_thesis: ex w being Element of W st A /\ C c= {w} then A /\ C c= { the Element of W} by XBOOLE_1:2; hence ex w being Element of W st A /\ C c= {w} ; ::_thesis: verum end; supposeA4: A /\ C <> {} ; ::_thesis: ex x being Element of W st A /\ C c= {x} set x = the Element of A /\ C; the Element of A /\ C in C by A4, XBOOLE_0:def_4; then reconsider x = the Element of A /\ C as Element of W ; take x = x; ::_thesis: A /\ C c= {x} thus A /\ C c= {x} ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A /\ C or y in {x} ) assume A5: y in A /\ C ; ::_thesis: y in {x} then y is Element of W ; then reconsider y9 = y as FinSequence of NAT ; x = y9 by A1, A5; hence y in {x} by TARSKI:def_1; ::_thesis: verum end; end; end; end; hence ex w being Element of W st A /\ C c= {w} ; ::_thesis: verum end; definition let W be Tree; let n be Nat; funcW -level n -> Level of W equals :: TREES_2:def 6 { w where w is Element of W : len w = n } ; coherence { w where w is Element of W : len w = n } is Level of W proof defpred S1[ Element of W] means len $1 = n; { w where w is Element of W : S1[w] } is Subset of W from DOMAIN_1:sch_7(); hence { w where w is Element of W : len w = n } is Level of W by Def4; ::_thesis: verum end; end; :: deftheorem defines -level TREES_2:def_6_:_ for W being Tree for n being Nat holds W -level n = { w where w is Element of W : len w = n } ; theorem :: TREES_2:12 for W being Tree for w being Element of W for n being Element of NAT holds ( w ^ <*n*> in succ w iff w ^ <*n*> in W ) ; theorem :: TREES_2:13 for W being Tree for w being Element of W st w = {} holds W -level 1 = succ w proof let W be Tree; ::_thesis: for w being Element of W st w = {} holds W -level 1 = succ w let w be Element of W; ::_thesis: ( w = {} implies W -level 1 = succ w ) assume A1: w = {} ; ::_thesis: W -level 1 = succ w thus W -level 1 c= succ w :: according to XBOOLE_0:def_10 ::_thesis: succ w c= W -level 1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W -level 1 or x in succ w ) assume x in W -level 1 ; ::_thesis: x in succ w then consider w9 being Element of W such that A2: x = w9 and A3: len w9 = 1 ; A4: w9 = <*(w9 . 1)*> by A3, FINSEQ_1:40; then rng w9 = {(w9 . 1)} by FINSEQ_1:39; then reconsider n = w9 . 1 as Element of NAT by ZFMISC_1:31; w9 = w ^ <*n*> by A1, A4, FINSEQ_1:34; hence x in succ w by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ w or x in W -level 1 ) assume x in succ w ; ::_thesis: x in W -level 1 then consider i being Element of NAT such that A5: x = w ^ <*i*> and A6: w ^ <*i*> in W ; reconsider w9 = w ^ <*i*> as Element of W by A6; ( len <*i*> = 1 & w9 = <*i*> ) by A1, FINSEQ_1:34, FINSEQ_1:39; hence x in W -level 1 by A5; ::_thesis: verum end; theorem Th14: :: TREES_2:14 for W being Tree holds W = union { (W -level n) where n is Element of NAT : verum } proof let W be Tree; ::_thesis: W = union { (W -level n) where n is Element of NAT : verum } thus W c= union { (W -level n) where n is Element of NAT : verum } :: according to XBOOLE_0:def_10 ::_thesis: union { (W -level n) where n is Element of NAT : verum } c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in union { (W -level n) where n is Element of NAT : verum } ) assume x in W ; ::_thesis: x in union { (W -level n) where n is Element of NAT : verum } then reconsider w = x as Element of W ; A1: x in W -level (len w) ; W -level (len w) in { (W -level n) where n is Element of NAT : verum } ; hence x in union { (W -level n) where n is Element of NAT : verum } by A1, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (W -level n) where n is Element of NAT : verum } or x in W ) assume x in union { (W -level n) where n is Element of NAT : verum } ; ::_thesis: x in W then consider X being set such that A2: ( x in X & X in { (W -level n) where n is Element of NAT : verum } ) by TARSKI:def_4; ex n being Element of NAT st X = W -level n by A2; hence x in W by A2; ::_thesis: verum end; theorem :: TREES_2:15 for W being finite Tree holds W = union { (W -level n) where n is Element of NAT : n <= height W } proof let W be finite Tree; ::_thesis: W = union { (W -level n) where n is Element of NAT : n <= height W } thus W c= union { (W -level n) where n is Element of NAT : n <= height W } :: according to XBOOLE_0:def_10 ::_thesis: union { (W -level n) where n is Element of NAT : n <= height W } c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in union { (W -level n) where n is Element of NAT : n <= height W } ) assume x in W ; ::_thesis: x in union { (W -level n) where n is Element of NAT : n <= height W } then reconsider w = x as Element of W ; A1: len w <= height W by TREES_1:def_12; A2: w in W -level (len w) ; W -level (len w) in { (W -level n) where n is Element of NAT : n <= height W } by A1; hence x in union { (W -level n) where n is Element of NAT : n <= height W } by A2, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (W -level n) where n is Element of NAT : n <= height W } or x in W ) assume x in union { (W -level n) where n is Element of NAT : n <= height W } ; ::_thesis: x in W then consider X being set such that A3: ( x in X & X in { (W -level n) where n is Element of NAT : n <= height W } ) by TARSKI:def_4; ex n being Element of NAT st ( X = W -level n & n <= height W ) by A3; hence x in W by A3; ::_thesis: verum end; theorem :: TREES_2:16 for W being Tree for L being Level of W ex n being Element of NAT st L = W -level n proof let W be Tree; ::_thesis: for L being Level of W ex n being Element of NAT st L = W -level n let L be Level of W; ::_thesis: ex n being Element of NAT st L = W -level n consider n being Nat such that A1: L = { w where w is Element of W : len w = n } by Def4; reconsider n = n as Element of NAT by ORDINAL1:def_12; take n ; ::_thesis: L = W -level n thus L = W -level n by A1; ::_thesis: verum end; scheme :: TREES_2:sch 2 FraenkelCard{ F1() -> non empty set , F2() -> set , F3( set ) -> set } : card { F3(w) where w is Element of F1() : w in F2() } c= card F2() proof consider f being Function such that A1: ( dom f = F2() & ( for x being set st x in F2() holds f . x = F3(x) ) ) from FUNCT_1:sch_3(); { F3(w) where w is Element of F1() : w in F2() } c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(w) where w is Element of F1() : w in F2() } or x in rng f ) assume x in { F3(w) where w is Element of F1() : w in F2() } ; ::_thesis: x in rng f then consider w being Element of F1() such that A2: x = F3(w) and A3: w in F2() ; f . w = x by A1, A2, A3; hence x in rng f by A1, A3, FUNCT_1:def_3; ::_thesis: verum end; hence card { F3(w) where w is Element of F1() : w in F2() } c= card F2() by A1, CARD_1:12; ::_thesis: verum end; scheme :: TREES_2:sch 3 FraenkelFinCard{ F1() -> non empty set , F2() -> finite set , F3() -> finite set , F4( set ) -> set } : card F3() <= card F2() provided A1: F3() = { F4(w) where w is Element of F1() : w in F2() } proof card { F4(w) where w is Element of F1() : w in F2() } c= card F2() from TREES_2:sch_2(); hence card F3() <= card F2() by A1, NAT_1:39; ::_thesis: verum end; theorem Th17: :: TREES_2:17 for W being Tree st W is finite-order holds ex n being Element of NAT st for w being Element of W ex B being finite set st ( B = succ w & card B <= n ) proof let W be Tree; ::_thesis: ( W is finite-order implies ex n being Element of NAT st for w being Element of W ex B being finite set st ( B = succ w & card B <= n ) ) given n being Element of NAT such that A1: for w being Element of W holds not w ^ <*n*> in W ; :: according to TREES_2:def_2 ::_thesis: ex n being Element of NAT st for w being Element of W ex B being finite set st ( B = succ w & card B <= n ) A2: Seg n is finite ; take n ; ::_thesis: for w being Element of W ex B being finite set st ( B = succ w & card B <= n ) let w be Element of W; ::_thesis: ex B being finite set st ( B = succ w & card B <= n ) deffunc H1( Real) -> set = w ^ <*($1 - 1)*>; A3: { H1(r) where r is Real : r in Seg n } is finite from FRAENKEL:sch_21(A2); A4: succ w c= { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ w or x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } ) assume x in succ w ; ::_thesis: x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } then consider k being Element of NAT such that A5: x = w ^ <*k*> and A6: w ^ <*k*> in W ; not w ^ <*n*> in W by A1; then k < n by A6, TREES_1:def_3; then A7: k + 1 <= n by NAT_1:13; 1 <= k + 1 by NAT_1:11; then A8: k + 1 in Seg n by A7, FINSEQ_1:1; (k + 1) - 1 = k ; hence x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } by A5, A8; ::_thesis: verum end; then reconsider B = succ w as finite set by A3; take B ; ::_thesis: ( B = succ w & card B <= n ) thus B = succ w ; ::_thesis: card B <= n set C = { H1(r) where r is Real : r in Seg n } ; { H1(r) where r is Real : r in Seg n } is finite from FRAENKEL:sch_21(A2); then reconsider C = { H1(r) where r is Real : r in Seg n } as finite set ; A9: C = { H1(r) where r is Real : r in Seg n } ; card C <= card (Seg n) from TREES_2:sch_3(A9); then A10: card C <= n by FINSEQ_1:57; card B <= card C by A4, NAT_1:43; hence card B <= n by A10, XXREAL_0:2; ::_thesis: verum end; theorem Th18: :: TREES_2:18 for W being Tree for w being Element of W st W is finite-order holds succ w is finite proof let W be Tree; ::_thesis: for w being Element of W st W is finite-order holds succ w is finite let w be Element of W; ::_thesis: ( W is finite-order implies succ w is finite ) assume W is finite-order ; ::_thesis: succ w is finite then consider n being Element of NAT such that A1: for w being Element of W ex B being finite set st ( B = succ w & card B <= n ) by Th17; ex B being finite set st ( B = succ w & card B <= n ) by A1; hence succ w is finite ; ::_thesis: verum end; registration let W be finite-order Tree; let w be Element of W; cluster succ w -> finite ; coherence succ w is finite by Th18; end; theorem Th19: :: TREES_2:19 for W being Tree holds {} is Chain of W proof let W be Tree; ::_thesis: {} is Chain of W reconsider S = {} as Subset of W by XBOOLE_1:2; S is Chain of W proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in S & q in S holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in S & q in S implies p,q are_c=-comparable ) thus ( p in S & q in S implies p,q are_c=-comparable ) ; ::_thesis: verum end; hence {} is Chain of W ; ::_thesis: verum end; theorem Th20: :: TREES_2:20 for W being Tree holds {{}} is Chain of W proof let W be Tree; ::_thesis: {{}} is Chain of W {} in W by TREES_1:22; then reconsider S = {{}} as Subset of W by ZFMISC_1:31; S is Chain of W proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in S & q in S holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in S & q in S implies p,q are_c=-comparable ) assume that A1: p in S and A2: q in S ; ::_thesis: p,q are_c=-comparable p = {} by A1, TARSKI:def_1; hence p,q are_c=-comparable by A2, TARSKI:def_1; ::_thesis: verum end; hence {{}} is Chain of W ; ::_thesis: verum end; registration let W be Tree; cluster non empty for Chain of W; existence not for b1 being Chain of W holds b1 is empty proof {{}} is Chain of W by Th20; hence not for b1 being Chain of W holds b1 is empty ; ::_thesis: verum end; end; definition let W be Tree; let IT be Chain of W; attrIT is Branch-like means :Def7: :: TREES_2:def 7 ( ( for p being FinSequence of NAT st p in IT holds ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds ( not p in W or ex q being FinSequence of NAT st ( q in IT & not q is_a_proper_prefix_of p ) ) ) ); end; :: deftheorem Def7 defines Branch-like TREES_2:def_7_:_ for W being Tree for IT being Chain of W holds ( IT is Branch-like iff ( ( for p being FinSequence of NAT st p in IT holds ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT holds ( not p in W or ex q being FinSequence of NAT st ( q in IT & not q is_a_proper_prefix_of p ) ) ) ) ); registration let W be Tree; cluster Branch-like for Chain of W; existence ex b1 being Chain of W st b1 is Branch-like proof defpred S1[ set ] means ( W is Chain of W & ( for p being FinSequence of NAT st p in W holds ProperPrefixes p c= W ) ); consider X being set such that A1: for Y being set holds ( Y in X iff ( Y in bool W & S1[Y] ) ) from XBOOLE_0:sch_1(); ( {} is Chain of W & ( for p being FinSequence of NAT st p in {} holds ProperPrefixes p c= {} ) ) by Th19; then A2: X <> {} by A1; now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_X_&_Z_is_c=-linear_holds_ union_Z_in_X let Z be set ; ::_thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X ) assume that Z <> {} and A3: Z c= X and A4: Z is c=-linear ; ::_thesis: union Z in X union Z c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in W ) assume x in union Z ; ::_thesis: x in W then consider Y being set such that A5: x in Y and A6: Y in Z by TARSKI:def_4; Y in bool W by A1, A3, A6; hence x in W by A5; ::_thesis: verum end; then reconsider Z9 = union Z as Subset of W ; A7: Z9 is Chain of W proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in Z9 & q in Z9 holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in Z9 & q in Z9 implies p,q are_c=-comparable ) assume p in Z9 ; ::_thesis: ( not q in Z9 or p,q are_c=-comparable ) then consider X1 being set such that A8: p in X1 and A9: X1 in Z by TARSKI:def_4; assume q in Z9 ; ::_thesis: p,q are_c=-comparable then consider X2 being set such that A10: q in X2 and A11: X2 in Z by TARSKI:def_4; X1,X2 are_c=-comparable by A4, A9, A11, ORDINAL1:def_8; then A12: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; A13: X1 is Chain of W by A1, A3, A9; X2 is Chain of W by A1, A3, A11; hence p,q are_c=-comparable by A8, A10, A12, A13, Def3; ::_thesis: verum end; now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_union_Z_holds_ ProperPrefixes_p_c=_union_Z let p be FinSequence of NAT ; ::_thesis: ( p in union Z implies ProperPrefixes p c= union Z ) assume p in union Z ; ::_thesis: ProperPrefixes p c= union Z then consider X1 being set such that A14: ( p in X1 & X1 in Z ) by TARSKI:def_4; ( ProperPrefixes p c= X1 & X1 c= union Z ) by A1, A3, A14, ZFMISC_1:74; hence ProperPrefixes p c= union Z by XBOOLE_1:1; ::_thesis: verum end; hence union Z in X by A1, A7; ::_thesis: verum end; then consider Y being set such that A15: Y in X and A16: for Z being set st Z in X & Z <> Y holds not Y c= Z by A2, ORDERS_1:67; reconsider Y = Y as Chain of W by A1, A15; take Y ; ::_thesis: Y is Branch-like thus for p being FinSequence of NAT st p in Y holds ProperPrefixes p c= Y by A1, A15; :: according to TREES_2:def_7 ::_thesis: for p being FinSequence of NAT holds ( not p in W or ex q being FinSequence of NAT st ( q in Y & not q is_a_proper_prefix_of p ) ) given p being FinSequence of NAT such that A17: p in W and A18: for q being FinSequence of NAT st q in Y holds q is_a_proper_prefix_of p ; ::_thesis: contradiction set Z = (ProperPrefixes p) \/ {p}; ( ProperPrefixes p c= W & {p} c= W ) by A17, TREES_1:def_3, ZFMISC_1:31; then reconsider Z9 = (ProperPrefixes p) \/ {p} as Subset of W by XBOOLE_1:8; A19: Z9 is Chain of W proof let q be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st q in Z9 & q in Z9 holds q,q are_c=-comparable let r be FinSequence of NAT ; ::_thesis: ( q in Z9 & r in Z9 implies q,r are_c=-comparable ) assume that A20: q in Z9 and A21: r in Z9 ; ::_thesis: q,r are_c=-comparable A22: ( q in ProperPrefixes p or q in {p} ) by A20, XBOOLE_0:def_3; A23: ( r in ProperPrefixes p or r in {p} ) by A21, XBOOLE_0:def_3; A24: ( q is_a_proper_prefix_of p or q = p ) by A22, TARSKI:def_1, TREES_1:12; A25: ( r is_a_proper_prefix_of p or r = p ) by A23, TARSKI:def_1, TREES_1:12; A26: q is_a_prefix_of p by A24, XBOOLE_0:def_8; r is_a_prefix_of p by A25, XBOOLE_0:def_8; hence q,r are_c=-comparable by A26, Th1; ::_thesis: verum end; now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_(ProperPrefixes_p)_\/_{p}_holds_ ProperPrefixes_q_c=_(ProperPrefixes_p)_\/_{p} let q be FinSequence of NAT ; ::_thesis: ( q in (ProperPrefixes p) \/ {p} implies ProperPrefixes q c= (ProperPrefixes p) \/ {p} ) assume q in (ProperPrefixes p) \/ {p} ; ::_thesis: ProperPrefixes q c= (ProperPrefixes p) \/ {p} then ( q in ProperPrefixes p or q in {p} ) by XBOOLE_0:def_3; then ( q is_a_proper_prefix_of p or q = p ) by TARSKI:def_1, TREES_1:12; then q is_a_prefix_of p by XBOOLE_0:def_8; then A27: ProperPrefixes q c= ProperPrefixes p by TREES_1:17; ProperPrefixes p c= (ProperPrefixes p) \/ {p} by XBOOLE_1:7; hence ProperPrefixes q c= (ProperPrefixes p) \/ {p} by A27, XBOOLE_1:1; ::_thesis: verum end; then A28: (ProperPrefixes p) \/ {p} in X by A1, A19; A29: p in {p} by TARSKI:def_1; A30: not p in Y by A18; A31: p in (ProperPrefixes p) \/ {p} by A29, XBOOLE_0:def_3; Y c= (ProperPrefixes p) \/ {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in (ProperPrefixes p) \/ {p} ) assume A32: x in Y ; ::_thesis: x in (ProperPrefixes p) \/ {p} then reconsider t = x as Element of W ; t is_a_proper_prefix_of p by A18, A32; then t in ProperPrefixes p by TREES_1:12; hence x in (ProperPrefixes p) \/ {p} by XBOOLE_0:def_3; ::_thesis: verum end; hence contradiction by A16, A28, A30, A31; ::_thesis: verum end; end; definition let W be Tree; mode Branch of W is Branch-like Chain of W; end; registration let W be Tree; cluster Branch-like -> non empty for Chain of W; coherence for b1 being Chain of W st b1 is Branch-like holds not b1 is empty proof let B be Chain of W; ::_thesis: ( B is Branch-like implies not B is empty ) assume A1: ( B is Branch-like & B is empty ) ; ::_thesis: contradiction set t = the Element of W; for q being FinSequence of NAT st q in B holds q is_a_proper_prefix_of the Element of W by A1; hence contradiction by A1, Def7; ::_thesis: verum end; end; theorem Th21: :: TREES_2:21 for W being Tree for v1, v2 being FinSequence for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds v2 is_a_prefix_of v1 proof let W be Tree; ::_thesis: for v1, v2 being FinSequence for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds v2 is_a_prefix_of v1 let v1, v2 be FinSequence; ::_thesis: for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds v2 is_a_prefix_of v1 let C be Chain of W; ::_thesis: ( v1 in C & v2 in C & not v1 in ProperPrefixes v2 implies v2 is_a_prefix_of v1 ) assume A1: ( v1 in C & v2 in C ) ; ::_thesis: ( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 ) then reconsider p = v1, q = v2 as Element of W ; assume A2: not v1 in ProperPrefixes v2 ; ::_thesis: v2 is_a_prefix_of v1 A3: p,q are_c=-comparable by A1, Def3; A4: not v1 is_a_proper_prefix_of v2 by A2, TREES_1:12; ( v1 is_a_prefix_of v2 or v2 is_a_prefix_of v1 ) by A3, XBOOLE_0:def_9; hence v2 is_a_prefix_of v1 by A4, XBOOLE_0:def_8; ::_thesis: verum end; theorem Th22: :: TREES_2:22 for W being Tree for v1, v2, v being FinSequence for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds v is_a_prefix_of v1 proof let W be Tree; ::_thesis: for v1, v2, v being FinSequence for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds v is_a_prefix_of v1 let v1, v2, v be FinSequence; ::_thesis: for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds v is_a_prefix_of v1 let C be Chain of W; ::_thesis: ( v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v implies v is_a_prefix_of v1 ) assume that A1: ( v1 in C & v2 in C ) and A2: v is_a_prefix_of v2 ; ::_thesis: ( v1 in ProperPrefixes v or v is_a_prefix_of v1 ) ( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 ) by A1, Th21; then ( v1 is_a_proper_prefix_of v2 or v is_a_prefix_of v1 ) by A2, TREES_1:12, XBOOLE_1:1; then v,v1 are_c=-comparable by A2, Th2, XBOOLE_0:def_9; then ( v is_a_proper_prefix_of v1 or v = v1 or v1 is_a_proper_prefix_of v ) by XBOOLE_1:104; hence ( v1 in ProperPrefixes v or v is_a_prefix_of v1 ) by TREES_1:12, XBOOLE_0:def_8; ::_thesis: verum end; registration let W be Tree; cluster finite for Chain of W; existence ex b1 being Chain of W st b1 is finite proof reconsider C = {} as Chain of W by Th19; take C ; ::_thesis: C is finite thus C is finite ; ::_thesis: verum end; end; theorem Th23: :: TREES_2:23 for W being Tree for n being Element of NAT for C being finite Chain of W st card C > n holds ex p being FinSequence of NAT st ( p in C & len p >= n ) proof let W be Tree; ::_thesis: for n being Element of NAT for C being finite Chain of W st card C > n holds ex p being FinSequence of NAT st ( p in C & len p >= n ) let n be Element of NAT ; ::_thesis: for C being finite Chain of W st card C > n holds ex p being FinSequence of NAT st ( p in C & len p >= n ) let C be finite Chain of W; ::_thesis: ( card C > n implies ex p being FinSequence of NAT st ( p in C & len p >= n ) ) defpred S1[ Element of NAT ] means ( $1 < card C implies ex p being FinSequence of NAT st ( p in C & len p >= $1 ) ); A1: S1[ 0 ] proof assume A2: 0 < card C ; ::_thesis: ex p being FinSequence of NAT st ( p in C & len p >= 0 ) then A3: C <> {} ; set x = the Element of C; reconsider x = the Element of C as Element of W by A2, CARD_1:27, TARSKI:def_3; reconsider x = x as FinSequence of NAT ; take x ; ::_thesis: ( x in C & len x >= 0 ) thus ( x in C & len x >= 0 ) by A3; ::_thesis: verum end; A4: 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 that A5: ( k < card C implies ex p being FinSequence of NAT st ( p in C & len p >= k ) ) and A6: k + 1 < card C ; ::_thesis: ex p being FinSequence of NAT st ( p in C & len p >= k + 1 ) A7: k <= k + 1 by NAT_1:11; then A8: k < card C by A6, XXREAL_0:2; consider p being FinSequence of NAT such that A9: p in C and A10: len p >= k by A5, A6, A7, XXREAL_0:2; reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:15; A11: len q = k by A10, FINSEQ_1:17; then A12: card (ProperPrefixes q) = k by TREES_1:35; then card (ProperPrefixes q) in card C by A8, NAT_1:44; then A13: C \ (ProperPrefixes q) <> {} by CARD_1:68; set x = the Element of C \ (ProperPrefixes q); A14: the Element of C \ (ProperPrefixes q) in C by A13, XBOOLE_0:def_5; A15: not the Element of C \ (ProperPrefixes q) in ProperPrefixes q by A13, XBOOLE_0:def_5; reconsider x = the Element of C \ (ProperPrefixes q) as Element of W by A14; card ((ProperPrefixes q) \/ {x}) = k + 1 by A12, A15, CARD_2:41; then card ((ProperPrefixes q) \/ {x}) in card C by A6, NAT_1:44; then A16: C \ ((ProperPrefixes q) \/ {x}) <> {} by CARD_1:68; set y = the Element of C \ ((ProperPrefixes q) \/ {x}); A17: the Element of C \ ((ProperPrefixes q) \/ {x}) in C by A16, XBOOLE_0:def_5; A18: not the Element of C \ ((ProperPrefixes q) \/ {x}) in (ProperPrefixes q) \/ {x} by A16, XBOOLE_0:def_5; reconsider y = the Element of C \ ((ProperPrefixes q) \/ {x}) as Element of W by A17; A19: not y in ProperPrefixes q by A18, XBOOLE_0:def_3; A20: not y in {x} by A18, XBOOLE_0:def_3; A21: q is_a_prefix_of p by TREES_1:def_1; then A22: q is_a_prefix_of x by A9, A14, A15, Th22; A23: q is_a_prefix_of y by A9, A17, A19, A21, Th22; A24: x <> y by A20, TARSKI:def_1; ( x = q or x <> q ) ; then ( q is_a_proper_prefix_of y or q is_a_proper_prefix_of x ) by A22, A23, A24, XBOOLE_0:def_8; then ( k < len x or k < len y ) by A11, TREES_1:6; then ( k + 1 <= len x or k + 1 <= len y ) by NAT_1:13; hence ex p being FinSequence of NAT st ( p in C & len p >= k + 1 ) by A14, A17; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A4); hence ( card C > n implies ex p being FinSequence of NAT st ( p in C & len p >= n ) ) ; ::_thesis: verum end; theorem Th24: :: TREES_2:24 for W being Tree for C being Chain of W holds { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } is Chain of W proof let W be Tree; ::_thesis: for C being Chain of W holds { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } is Chain of W let C be Chain of W; ::_thesis: { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } is Chain of W { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } or x in W ) assume x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ; ::_thesis: x in W then ex w being Element of W st ( x = w & ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) ) ; hence x in W ; ::_thesis: verum end; then reconsider Z = { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } as Subset of W ; Z is Chain of W proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in Z & q in Z holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in Z & q in Z implies p,q are_c=-comparable ) assume p in Z ; ::_thesis: ( not q in Z or p,q are_c=-comparable ) then ex w being Element of W st ( p = w & ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) ) ; then consider r1 being FinSequence of NAT such that A1: r1 in C and A2: p is_a_prefix_of r1 ; assume q in Z ; ::_thesis: p,q are_c=-comparable then ex w9 being Element of W st ( q = w9 & ex p being FinSequence of NAT st ( p in C & w9 is_a_prefix_of p ) ) ; then consider r2 being FinSequence of NAT such that A3: r2 in C and A4: q is_a_prefix_of r2 ; r1,r2 are_c=-comparable by A1, A3, Def3; then ( r1 is_a_prefix_of r2 or r2 is_a_prefix_of r1 ) by XBOOLE_0:def_9; then ( p is_a_prefix_of r2 or q is_a_prefix_of r1 ) by A2, A4, XBOOLE_1:1; hence p,q are_c=-comparable by A2, A4, Th1; ::_thesis: verum end; hence { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } is Chain of W ; ::_thesis: verum end; theorem Th25: :: TREES_2:25 for W being Tree for p, q being FinSequence of NAT for B being Branch of W st p is_a_prefix_of q & q in B holds p in B proof let W be Tree; ::_thesis: for p, q being FinSequence of NAT for B being Branch of W st p is_a_prefix_of q & q in B holds p in B let p, q be FinSequence of NAT ; ::_thesis: for B being Branch of W st p is_a_prefix_of q & q in B holds p in B let B be Branch of W; ::_thesis: ( p is_a_prefix_of q & q in B implies p in B ) assume p is_a_prefix_of q ; ::_thesis: ( not q in B or p in B ) then ( p is_a_proper_prefix_of q or p = q ) by XBOOLE_0:def_8; then A1: ( p in ProperPrefixes q or p = q ) by TREES_1:def_2; assume A2: q in B ; ::_thesis: p in B then ProperPrefixes q c= B by Def7; hence p in B by A1, A2; ::_thesis: verum end; theorem Th26: :: TREES_2:26 for W being Tree for B being Branch of W holds {} in B proof let W be Tree; ::_thesis: for B being Branch of W holds {} in B let B be Branch of W; ::_thesis: {} in B set x = the Element of B; reconsider x = the Element of B as Element of W ; <*> NAT is_a_prefix_of x by XBOOLE_1:2; hence {} in B by Th25; ::_thesis: verum end; theorem Th27: :: TREES_2:27 for W being Tree for p, q being FinSequence of NAT for C being Chain of W st p in C & q in C & len p <= len q holds p is_a_prefix_of q proof let W be Tree; ::_thesis: for p, q being FinSequence of NAT for C being Chain of W st p in C & q in C & len p <= len q holds p is_a_prefix_of q let p, q be FinSequence of NAT ; ::_thesis: for C being Chain of W st p in C & q in C & len p <= len q holds p is_a_prefix_of q let C be Chain of W; ::_thesis: ( p in C & q in C & len p <= len q implies p is_a_prefix_of q ) assume ( p in C & q in C & len p <= len q & not p is_a_prefix_of q ) ; ::_thesis: contradiction then ( q in ProperPrefixes p & not q is_a_proper_prefix_of p ) by Th21, TREES_1:6; hence contradiction by TREES_1:12; ::_thesis: verum end; theorem Th28: :: TREES_2:28 for W being Tree for C being Chain of W ex B being Branch of W st C c= B proof let W be Tree; ::_thesis: for C being Chain of W ex B being Branch of W st C c= B let C be Chain of W; ::_thesis: ex B being Branch of W st C c= B defpred S1[ set ] means ( $1 is Chain of W & C c= $1 & ( for p being FinSequence of NAT st p in $1 holds ProperPrefixes p c= $1 ) ); consider X being set such that A1: for Y being set holds ( Y in X iff ( Y in bool W & S1[Y] ) ) from XBOOLE_0:sch_1(); set Z = { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ; A2: { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } is Chain of W by Th24; A3: C c= { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ) assume A4: x in C ; ::_thesis: x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } then reconsider w = x as Element of W ; w is_a_prefix_of w ; hence x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } by A4; ::_thesis: verum end; now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in__{__w_where_w_is_Element_of_W_:_ex_p_being_FinSequence_of_NAT_st_ (_p_in_C_&_w_is_a_prefix_of_p_)__}__holds_ ProperPrefixes_p_c=__{__w_where_w_is_Element_of_W_:_ex_p_being_FinSequence_of_NAT_st_ (_p_in_C_&_w_is_a_prefix_of_p_)__}_ let p be FinSequence of NAT ; ::_thesis: ( p in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } implies ProperPrefixes p c= { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ) assume p in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ; ::_thesis: ProperPrefixes p c= { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } then A5: ex w being Element of W st ( p = w & ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) ) ; then consider q being FinSequence of NAT such that A6: q in C and A7: p is_a_prefix_of q ; thus ProperPrefixes p c= { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes p or x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } ) assume x in ProperPrefixes p ; ::_thesis: x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } then consider r being FinSequence such that A8: x = r and A9: r is_a_proper_prefix_of p by TREES_1:def_2; r is_a_prefix_of p by A9, XBOOLE_0:def_8; then ( r is_a_prefix_of q & r in W ) by A5, A7, TREES_1:20, XBOOLE_1:1; hence x in { w where w is Element of W : ex p being FinSequence of NAT st ( p in C & w is_a_prefix_of p ) } by A6, A8; ::_thesis: verum end; end; then A10: X <> {} by A1, A2, A3; now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_X_&_Z_is_c=-linear_holds_ union_Z_in_X let Z be set ; ::_thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X ) assume that A11: Z <> {} and A12: Z c= X and A13: Z is c=-linear ; ::_thesis: union Z in X union Z c= W proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in W ) assume x in union Z ; ::_thesis: x in W then consider Y being set such that A14: x in Y and A15: Y in Z by TARSKI:def_4; Y in bool W by A1, A12, A15; hence x in W by A14; ::_thesis: verum end; then reconsider Z9 = union Z as Subset of W ; A16: Z9 is Chain of W proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in Z9 & q in Z9 holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in Z9 & q in Z9 implies p,q are_c=-comparable ) assume p in Z9 ; ::_thesis: ( not q in Z9 or p,q are_c=-comparable ) then consider X1 being set such that A17: p in X1 and A18: X1 in Z by TARSKI:def_4; assume q in Z9 ; ::_thesis: p,q are_c=-comparable then consider X2 being set such that A19: q in X2 and A20: X2 in Z by TARSKI:def_4; X1,X2 are_c=-comparable by A13, A18, A20, ORDINAL1:def_8; then A21: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; A22: X1 is Chain of W by A1, A12, A18; X2 is Chain of W by A1, A12, A20; hence p,q are_c=-comparable by A17, A19, A21, A22, Def3; ::_thesis: verum end; A23: now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_union_Z_holds_ ProperPrefixes_p_c=_union_Z let p be FinSequence of NAT ; ::_thesis: ( p in union Z implies ProperPrefixes p c= union Z ) assume p in union Z ; ::_thesis: ProperPrefixes p c= union Z then consider X1 being set such that A24: ( p in X1 & X1 in Z ) by TARSKI:def_4; ( ProperPrefixes p c= X1 & X1 c= union Z ) by A1, A12, A24, ZFMISC_1:74; hence ProperPrefixes p c= union Z by XBOOLE_1:1; ::_thesis: verum end; set x = the Element of Z; the Element of Z in X by A11, A12, TARSKI:def_3; then A25: C c= the Element of Z by A1; the Element of Z c= union Z by A11, ZFMISC_1:74; then C c= union Z by A25, XBOOLE_1:1; hence union Z in X by A1, A16, A23; ::_thesis: verum end; then consider Y being set such that A26: Y in X and A27: for Z being set st Z in X & Z <> Y holds not Y c= Z by A10, ORDERS_1:67; reconsider Y = Y as Chain of W by A1, A26; now__::_thesis:_(_(_for_p_being_FinSequence_of_NAT_st_p_in_Y_holds_ ProperPrefixes_p_c=_Y_)_&_(_for_p_being_FinSequence_of_NAT_holds_ (_not_p_in_W_or_ex_q_being_FinSequence_of_NAT_st_ (_q_in_Y_&_not_q_is_a_proper_prefix_of_p_)_)_)_) thus for p being FinSequence of NAT st p in Y holds ProperPrefixes p c= Y by A1, A26; ::_thesis: for p being FinSequence of NAT holds ( not p in W or ex q being FinSequence of NAT st ( q in Y & not q is_a_proper_prefix_of p ) ) given p being FinSequence of NAT such that A28: p in W and A29: for q being FinSequence of NAT st q in Y holds q is_a_proper_prefix_of p ; ::_thesis: contradiction set Z = (ProperPrefixes p) \/ {p}; ( ProperPrefixes p c= W & {p} c= W ) by A28, TREES_1:def_3, ZFMISC_1:31; then reconsider Z9 = (ProperPrefixes p) \/ {p} as Subset of W by XBOOLE_1:8; A30: Z9 is Chain of W proof let q be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st q in Z9 & q in Z9 holds q,q are_c=-comparable let r be FinSequence of NAT ; ::_thesis: ( q in Z9 & r in Z9 implies q,r are_c=-comparable ) assume that A31: q in Z9 and A32: r in Z9 ; ::_thesis: q,r are_c=-comparable A33: ( q in ProperPrefixes p or q in {p} ) by A31, XBOOLE_0:def_3; A34: ( r in ProperPrefixes p or r in {p} ) by A32, XBOOLE_0:def_3; A35: ( q is_a_proper_prefix_of p or q = p ) by A33, TARSKI:def_1, TREES_1:12; A36: ( r is_a_proper_prefix_of p or r = p ) by A34, TARSKI:def_1, TREES_1:12; A37: q is_a_prefix_of p by A35, XBOOLE_0:def_8; r is_a_prefix_of p by A36, XBOOLE_0:def_8; hence q,r are_c=-comparable by A37, Th1; ::_thesis: verum end; A38: now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_(ProperPrefixes_p)_\/_{p}_holds_ ProperPrefixes_q_c=_(ProperPrefixes_p)_\/_{p} let q be FinSequence of NAT ; ::_thesis: ( q in (ProperPrefixes p) \/ {p} implies ProperPrefixes q c= (ProperPrefixes p) \/ {p} ) assume q in (ProperPrefixes p) \/ {p} ; ::_thesis: ProperPrefixes q c= (ProperPrefixes p) \/ {p} then ( q in ProperPrefixes p or q in {p} ) by XBOOLE_0:def_3; then ( q is_a_proper_prefix_of p or q = p ) by TARSKI:def_1, TREES_1:12; then q is_a_prefix_of p by XBOOLE_0:def_8; then A39: ProperPrefixes q c= ProperPrefixes p by TREES_1:17; ProperPrefixes p c= (ProperPrefixes p) \/ {p} by XBOOLE_1:7; hence ProperPrefixes q c= (ProperPrefixes p) \/ {p} by A39, XBOOLE_1:1; ::_thesis: verum end; A40: Y c= (ProperPrefixes p) \/ {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in (ProperPrefixes p) \/ {p} ) assume A41: x in Y ; ::_thesis: x in (ProperPrefixes p) \/ {p} then reconsider t = x as Element of W ; t is_a_proper_prefix_of p by A29, A41; then t in ProperPrefixes p by TREES_1:12; hence x in (ProperPrefixes p) \/ {p} by XBOOLE_0:def_3; ::_thesis: verum end; C c= Y by A1, A26; then C c= (ProperPrefixes p) \/ {p} by A40, XBOOLE_1:1; then A42: (ProperPrefixes p) \/ {p} in X by A1, A30, A38; A43: p in {p} by TARSKI:def_1; A44: not p in Y by A29; p in (ProperPrefixes p) \/ {p} by A43, XBOOLE_0:def_3; hence contradiction by A27, A40, A42, A44; ::_thesis: verum end; then reconsider Y = Y as Branch of W by Def7; take Y ; ::_thesis: C c= Y thus C c= Y by A1, A26; ::_thesis: verum end; scheme :: TREES_2:sch 4 FuncExOfMinNat{ P1[ set , Nat], F1() -> set } : ex f being Function st ( dom f = F1() & ( for x being set st x in F1() holds ex n being Element of NAT st ( f . x = n & P1[x,n] & ( for m being Element of NAT st P1[x,m] holds n <= m ) ) ) ) provided A1: for x being set st x in F1() holds ex n being Element of NAT st P1[x,n] proof defpred S1[ set , set ] means ex n being Element of NAT st ( $2 = n & P1[$1,n] & ( for m being Element of NAT st P1[$1,m] holds n <= m ) ); A2: 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] ) defpred S2[ Nat] means P1[x,$1]; assume x in F1() ; ::_thesis: ex y being set st S1[x,y] then ex n being Element of NAT st S2[n] by A1; then A3: ex n being Nat st S2[n] ; consider n being Nat such that A4: ( S2[n] & ( for m being Nat st S2[m] holds n <= m ) ) from NAT_1:sch_5(A3); take n ; ::_thesis: S1[x,n] ( n in NAT & ( for m being Element of NAT st S2[m] holds n <= m ) ) by A4, ORDINAL1:def_12; hence S1[x,n] by A4; ::_thesis: verum end; thus 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(A2); ::_thesis: verum end; Lm1: for X being set st X is finite holds ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n proof let X be set ; ::_thesis: ( X is finite implies ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n ) assume A1: X is finite ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n defpred S1[ set , set ] means ex k1, k2 being Element of NAT st ( $1 = k1 & $2 = k2 & k1 >= k2 ); now__::_thesis:_ex_n_being_Element_of_NAT_st_ for_k_being_Element_of_NAT_st_k_in_X_holds_ k_<=_n percases ( X /\ NAT = {} or X /\ NAT <> {} ) ; supposeA2: X /\ NAT = {} ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n thus ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n ::_thesis: verum proof take 0 ; ::_thesis: for k being Element of NAT st k in X holds k <= 0 let k be Element of NAT ; ::_thesis: ( k in X implies k <= 0 ) assume k in X ; ::_thesis: k <= 0 hence k <= 0 by A2, XBOOLE_0:def_4; ::_thesis: verum end; end; supposeA3: X /\ NAT <> {} ; ::_thesis: ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n reconsider XN = X /\ NAT as finite set by A1; A4: XN <> {} by A3; A5: for x, y being set st S1[x,y] & S1[y,x] holds x = y by XXREAL_0:1; A6: for x, y, z being set st S1[x,y] & S1[y,z] holds S1[x,z] by XXREAL_0:2; consider x being set such that A7: ( x in XN & ( for y being set st y in XN & y <> x holds not S1[y,x] ) ) from CARD_2:sch_1(A4, A5, A6); reconsider n = x as Element of NAT by A7, XBOOLE_0:def_4; take n = n; ::_thesis: for k being Element of NAT st k in X holds k <= n let k be Element of NAT ; ::_thesis: ( k in X implies k <= n ) assume k in X ; ::_thesis: k <= n then k in X /\ NAT by XBOOLE_0:def_4; hence k <= n by A7; ::_thesis: verum end; end; end; hence ex n being Element of NAT st for k being Element of NAT st k in X holds k <= n ; ::_thesis: verum end; scheme :: TREES_2:sch 5 InfiniteChain{ F1() -> set , F2() -> set , P1[ set ], P2[ set , set ] } : ex f being Function st ( dom f = NAT & rng f c= F1() & f . 0 = F2() & ( for k being Element of NAT holds ( P2[f . k,f . (k + 1)] & P1[f . k] ) ) ) provided A1: ( F2() in F1() & P1[F2()] ) and A2: for x being set st x in F1() & P1[x] holds ex y being set st ( y in F1() & P2[x,y] & P1[y] ) proof consider Y being set such that A3: for x being set holds ( x in Y iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1(); defpred S1[ set , set ] means ( $2 in Y & P2[$1,$2] ); A4: for x being set st x in Y holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Y implies ex y being set st S1[x,y] ) assume x in Y ; ::_thesis: ex y being set st S1[x,y] then ( x in F1() & P1[x] ) by A3; then consider y being set such that A5: ( y in F1() & P2[x,y] & P1[y] ) by A2; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A3, A5; ::_thesis: verum end; consider g being Function such that A6: ( dom g = Y & ( for x being set st x in Y holds S1[x,g . x] ) ) from CLASSES1:sch_1(A4); deffunc H1( set , set ) -> set = g . $2; consider f being Function such that A7: ( dom f = NAT & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_11(); take f ; ::_thesis: ( dom f = NAT & rng f c= F1() & f . 0 = F2() & ( for k being Element of NAT holds ( P2[f . k,f . (k + 1)] & P1[f . k] ) ) ) thus dom f = NAT by A7; ::_thesis: ( rng f c= F1() & f . 0 = F2() & ( for k being Element of NAT holds ( P2[f . k,f . (k + 1)] & P1[f . k] ) ) ) defpred S2[ Element of NAT ] means f . $1 in Y; A8: S2[ 0 ] by A1, A3, A7; A9: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume f . k in Y ; ::_thesis: S2[k + 1] then g . (f . k) in Y by A6; hence S2[k + 1] by A7; ::_thesis: verum end; A10: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A8, A9); thus rng f c= F1() ::_thesis: ( f . 0 = F2() & ( for k being Element of NAT holds ( P2[f . k,f . (k + 1)] & P1[f . k] ) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F1() ) assume x in rng f ; ::_thesis: x in F1() then consider y being set such that A11: y in dom f and A12: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A7, A11; f . y in Y by A10; hence x in F1() by A3, A12; ::_thesis: verum end; thus f . 0 = F2() by A7; ::_thesis: for k being Element of NAT holds ( P2[f . k,f . (k + 1)] & P1[f . k] ) let k be Element of NAT ; ::_thesis: ( P2[f . k,f . (k + 1)] & P1[f . k] ) A13: f . k in Y by A10; then P2[f . k,g . (f . k)] by A6; hence ( P2[f . k,f . (k + 1)] & P1[f . k] ) by A3, A7, A13; ::_thesis: verum end; theorem Th29: :: TREES_2:29 for T being Tree st ( for n being Element of NAT ex C being finite Chain of T st card C = n ) & ( for t being Element of T holds succ t is finite ) holds ex B being Chain of T st not B is finite proof let T be Tree; ::_thesis: ( ( for n being Element of NAT ex C being finite Chain of T st card C = n ) & ( for t being Element of T holds succ t is finite ) implies ex B being Chain of T st not B is finite ) assume that A1: for n being Element of NAT ex X being finite Chain of T st card X = n and A2: for t being Element of T holds succ t is finite ; ::_thesis: not for B being Chain of T holds B is finite defpred S1[ FinSequence] means for n being Element of NAT ex B being Branch of T st ( $1 in B & ex p being FinSequence of NAT st ( p in B & len p >= (len $1) + n ) ); A3: for x being Element of T st S1[x] holds ex n being Element of NAT st ( x ^ <*n*> in T & S1[x ^ <*n*>] ) proof let x be Element of T; ::_thesis: ( S1[x] implies ex n being Element of NAT st ( x ^ <*n*> in T & S1[x ^ <*n*>] ) ) assume that A4: S1[x] and A5: for n being Element of NAT st x ^ <*n*> in T holds not S1[x ^ <*n*>] ; ::_thesis: contradiction A6: succ x is finite by A2; defpred S2[ set , Element of NAT ] means for B being Branch of T for p, q being FinSequence of NAT st p = $1 & $1 in B & q in B holds (len p) + $2 > len q; A7: for y being set st y in succ x holds ex n being Element of NAT st S2[y,n] proof let y be set ; ::_thesis: ( y in succ x implies ex n being Element of NAT st S2[y,n] ) assume y in succ x ; ::_thesis: ex n being Element of NAT st S2[y,n] then consider k being Element of NAT such that A8: y = x ^ <*k*> and A9: x ^ <*k*> in T ; consider n being Element of NAT such that A10: for B being Branch of T st x ^ <*k*> in B holds for p being FinSequence of NAT st p in B holds len p < (len (x ^ <*k*>)) + n by A5, A9; take n ; ::_thesis: S2[y,n] thus S2[y,n] by A8, A10; ::_thesis: verum end; consider f being Function such that A11: dom f = succ x and A12: for y being set st y in succ x holds ex n being Element of NAT st ( f . y = n & S2[y,n] & ( for m being Element of NAT st S2[y,m] holds n <= m ) ) from TREES_2:sch_4(A7); consider k being Element of NAT such that A13: for m being Element of NAT st m in rng f holds m <= k by A6, A11, Lm1, FINSET_1:8; consider B being Branch of T such that A14: x in B and A15: ex p being FinSequence of NAT st ( p in B & len p >= (len x) + (k + 1) ) by A4; consider p being FinSequence of NAT such that A16: p in B and A17: len p >= (len x) + (k + 1) by A15; reconsider r = p | (Seg ((len x) + 1)) as FinSequence of NAT by FINSEQ_1:18; (len x) + 1 <= ((len x) + 1) + k by NAT_1:11; then A18: len p >= (len x) + 1 by A17, XXREAL_0:2; A19: r is_a_prefix_of p by TREES_1:def_1; A20: len r = (len x) + 1 by A18, FINSEQ_1:17; A21: r in B by A16, A19, Th25; then x is_a_prefix_of r by A14, A20, Th27, NAT_1:11; then consider j being FinSequence such that A22: r = x ^ j by TREES_1:1; (len x) + (len j) = len r by A22, FINSEQ_1:22; then A23: j = <*(j . 1)*> by A20, FINSEQ_1:40; A24: ( dom r = Seg (len r) & 1 <= 1 + (len x) ) by FINSEQ_1:def_3, NAT_1:11; (len x) + 1 <= len r by A18, FINSEQ_1:17; then ( (x ^ <*(j . 1)*>) . ((len x) + 1) = j . 1 & (len x) + 1 in dom r ) by A24, FINSEQ_1:1, FINSEQ_1:42; then j . 1 in rng r by A22, A23, FUNCT_1:def_3; then reconsider l = j . 1 as Element of NAT ; A25: x ^ <*l*> in succ x by A21, A22, A23; then consider n being Element of NAT such that A26: f . (x ^ <*l*>) = n and A27: for B being Branch of T for p, q being FinSequence of NAT st p = x ^ <*l*> & x ^ <*l*> in B & q in B holds (len p) + n > len q and for m being Element of NAT st ( for B being Branch of T for p, q being FinSequence of NAT st p = x ^ <*l*> & x ^ <*l*> in B & q in B holds (len p) + m > len q ) holds n <= m by A12; n in rng f by A11, A25, A26, FUNCT_1:def_3; then n <= k by A13; then (len r) + n <= ((len x) + 1) + k by A20, XREAL_1:7; hence contradiction by A16, A17, A21, A22, A23, A27, XXREAL_0:2; ::_thesis: verum end; reconsider e = {} as Element of T by TREES_1:22; A28: S1[e] proof given n being Element of NAT such that A29: for B being Branch of T st e in B holds for p being FinSequence of NAT st p in B holds len p < (len e) + n ; ::_thesis: contradiction consider C being finite Chain of T such that A30: card C = n + 1 by A1; consider B being Branch of T such that A31: C c= B by Th28; n + 0 < n + 1 by XREAL_1:6; then A32: ex p being FinSequence of NAT st ( p in C & len p >= n ) by A30, Th23; ( e in B & len e = 0 ) by Th26; hence contradiction by A29, A31, A32; ::_thesis: verum end; defpred S2[ set ] means ex t being Element of T st ( t = $1 & S1[t] ); defpred S3[ set , set ] means ex p being FinSequence of NAT ex n being Element of NAT st ( $1 = p & p ^ <*n*> in T & $2 = p ^ <*n*> ); A33: ( e in T & S2[e] ) by A28; A34: for x being set st x in T & S2[x] holds ex y being set st ( y in T & S3[x,y] & S2[y] ) proof let x be set ; ::_thesis: ( x in T & S2[x] implies ex y being set st ( y in T & S3[x,y] & S2[y] ) ) assume x in T ; ::_thesis: ( not S2[x] or ex y being set st ( y in T & S3[x,y] & S2[y] ) ) given t being Element of T such that A35: t = x and A36: S1[t] ; ::_thesis: ex y being set st ( y in T & S3[x,y] & S2[y] ) consider n being Element of NAT such that A37: t ^ <*n*> in T and A38: S1[t ^ <*n*>] by A3, A36; reconsider y = t ^ <*n*> as set ; take y ; ::_thesis: ( y in T & S3[x,y] & S2[y] ) thus ( y in T & S3[x,y] ) by A35, A37; ::_thesis: S2[y] reconsider t1 = t ^ <*n*> as Element of T by A37; take t1 ; ::_thesis: ( t1 = y & S1[t1] ) thus ( t1 = y & S1[t1] ) by A38; ::_thesis: verum end; ex f being Function st ( dom f = NAT & rng f c= T & f . 0 = e & ( for k being Element of NAT holds ( S3[f . k,f . (k + 1)] & S2[f . k] ) ) ) from TREES_2:sch_5(A33, A34); then consider f being Function such that A39: dom f = NAT and A40: rng f c= T and A41: f . 0 = e and A42: for k being Element of NAT holds ( ex p being FinSequence of NAT ex n being Element of NAT st ( f . k = p & p ^ <*n*> in T & f . (k + 1) = p ^ <*n*> ) & ex t being Element of T st ( t = f . k & S1[t] ) ) ; reconsider C = rng f as Subset of T by A40; A43: now__::_thesis:_for_k,_n_being_Nat_holds_S4[n] let k be Nat; ::_thesis: for n being Nat holds S4[n] defpred S4[ Nat] means for p, q being FinSequence of NAT st p = f . k & q = f . (k + $1) holds p is_a_prefix_of q; A44: S4[ 0 ] ; A45: for n being Nat st S4[n] holds S4[n + 1] proof let n be Nat; ::_thesis: ( S4[n] implies S4[n + 1] ) assume A46: for p, q being FinSequence of NAT st p = f . k & q = f . (k + n) holds p is_a_prefix_of q ; ::_thesis: S4[n + 1] let p, q be FinSequence of NAT ; ::_thesis: ( p = f . k & q = f . (k + (n + 1)) implies p is_a_prefix_of q ) assume that A47: p = f . k and A48: q = f . (k + (n + 1)) ; ::_thesis: p is_a_prefix_of q reconsider k = k, n = n as Element of NAT by ORDINAL1:def_12; consider r being FinSequence of NAT , l being Element of NAT such that A49: f . (k + n) = r and r ^ <*l*> in T and A50: f . ((k + n) + 1) = r ^ <*l*> by A42; A51: p is_a_prefix_of r by A46, A47, A49; r is_a_prefix_of r ^ <*l*> by TREES_1:1; hence p is_a_prefix_of q by A48, A50, A51, XBOOLE_1:1; ::_thesis: verum end; thus for n being Nat holds S4[n] from NAT_1:sch_2(A44, A45); ::_thesis: verum end; A52: now__::_thesis:_for_k,_l_being_Element_of_NAT_st_k_<=_l_holds_ for_p,_q_being_FinSequence_of_NAT_st_p_=_f_._k_&_q_=_f_._l_holds_ p_is_a_prefix_of_q let k, l be Element of NAT ; ::_thesis: ( k <= l implies for p, q being FinSequence of NAT st p = f . k & q = f . l holds p is_a_prefix_of q ) assume k <= l ; ::_thesis: for p, q being FinSequence of NAT st p = f . k & q = f . l holds p is_a_prefix_of q then ex n being Nat st l = k + n by NAT_1:10; hence for p, q being FinSequence of NAT st p = f . k & q = f . l holds p is_a_prefix_of q by A43; ::_thesis: verum end; C is Chain of T proof let p be FinSequence of NAT ; :: according to TREES_2:def_3 ::_thesis: for q being FinSequence of NAT st p in C & q in C holds p,q are_c=-comparable let q be FinSequence of NAT ; ::_thesis: ( p in C & q in C implies p,q are_c=-comparable ) assume that A53: p in C and A54: q in C ; ::_thesis: p,q are_c=-comparable consider x being set such that A55: x in NAT and A56: p = f . x by A39, A53, FUNCT_1:def_3; consider y being set such that A57: y in NAT and A58: q = f . y by A39, A54, FUNCT_1:def_3; reconsider x = x, y = y as Element of NAT by A55, A57; ( x <= y or y <= x ) ; hence ( p is_a_prefix_of q or q is_a_prefix_of p ) by A52, A56, A58; :: according to XBOOLE_0:def_9 ::_thesis: verum end; then reconsider C = C as Chain of T ; take C ; ::_thesis: not C is finite defpred S4[ Element of NAT ] means for p being FinSequence of NAT st p = f . $1 holds len p = $1; A59: S4[ 0 ] by A41; A60: for k being Element of NAT st S4[k] holds S4[k + 1] proof let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] ) assume A61: for p being FinSequence of NAT st p = f . k holds len p = k ; ::_thesis: S4[k + 1] let p be FinSequence of NAT ; ::_thesis: ( p = f . (k + 1) implies len p = k + 1 ) assume A62: p = f . (k + 1) ; ::_thesis: len p = k + 1 consider q being FinSequence of NAT , n being Element of NAT such that A63: f . k = q and q ^ <*n*> in T and A64: f . (k + 1) = q ^ <*n*> by A42; thus len p = (len q) + (len <*n*>) by A62, A64, FINSEQ_1:22 .= (len q) + 1 by FINSEQ_1:39 .= k + 1 by A61, A63 ; ::_thesis: verum end; A65: for k being Element of NAT holds S4[k] from NAT_1:sch_1(A59, A60); f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y ) then reconsider x9 = x, y9 = y as Element of NAT by A39; consider p being FinSequence of NAT , n being Element of NAT such that A66: f . x9 = p and p ^ <*n*> in T and f . (x9 + 1) = p ^ <*n*> by A42; A67: ex q being FinSequence of NAT ex k being Element of NAT st ( f . y9 = q & q ^ <*k*> in T & f . (y9 + 1) = q ^ <*k*> ) by A42; len p = x9 by A65, A66; hence ( not f . x = f . y or x = y ) by A65, A66, A67; ::_thesis: verum end; then NAT ,C are_equipotent by A39, WELLORD2:def_4; hence not C is finite by CARD_1:38; ::_thesis: verum end; theorem :: TREES_2:30 for T being finite-order Tree st ( for n being Element of NAT ex C being finite Chain of T st card C = n ) holds ex B being Chain of T st not B is finite proof let T be finite-order Tree; ::_thesis: ( ( for n being Element of NAT ex C being finite Chain of T st card C = n ) implies ex B being Chain of T st not B is finite ) for t being Element of T holds succ t is finite ; hence ( ( for n being Element of NAT ex C being finite Chain of T st card C = n ) implies ex B being Chain of T st not B is finite ) by Th29; ::_thesis: verum end; definition let IT be Relation; attrIT is DecoratedTree-like means :Def8: :: TREES_2:def 8 dom IT is Tree; end; :: deftheorem Def8 defines DecoratedTree-like TREES_2:def_8_:_ for IT being Relation holds ( IT is DecoratedTree-like iff dom IT is Tree ); registration cluster Relation-like Function-like DecoratedTree-like for set ; existence ex b1 being Function st b1 is DecoratedTree-like proof set W = the Tree; take f = the Tree --> 0; ::_thesis: f is DecoratedTree-like thus dom f is Tree by FUNCOP_1:13; :: according to TREES_2:def_8 ::_thesis: verum end; end; definition mode DecoratedTree is DecoratedTree-like Function; end; registration let T be DecoratedTree; cluster dom T -> non empty Tree-like ; coherence ( not dom T is empty & dom T is Tree-like ) by Def8; end; registration let D be non empty set ; cluster Relation-like D -valued Function-like DecoratedTree-like for set ; existence ex b1 being Function st ( b1 is DecoratedTree-like & b1 is D -valued ) proof set W = the Tree; set d = the Element of D; set f = the Tree --> the Element of D; dom ( the Tree --> the Element of D) = the Tree by FUNCOP_1:13; then reconsider f = the Tree --> the Element of D as DecoratedTree by Def8; f is D -valued ; hence ex b1 being Function st ( b1 is DecoratedTree-like & b1 is D -valued ) ; ::_thesis: verum end; end; definition let D be non empty set ; mode DecoratedTree of D is D -valued DecoratedTree; end; definition let D be non empty set ; let T be DecoratedTree of D; let t be Element of dom T; :: original: . redefine funcT . t -> Element of D; coherence T . t is Element of D proof ( T . t in rng T & rng T c= D ) by FUNCT_1:def_3; hence T . t is Element of D ; ::_thesis: verum end; end; theorem Th31: :: TREES_2:31 for T1, T2 being DecoratedTree st dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds T1 . p = T2 . p ) holds T1 = T2 proof let T1, T2 be DecoratedTree; ::_thesis: ( dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds T1 . p = T2 . p ) implies T1 = T2 ) assume that A1: dom T1 = dom T2 and A2: for p being FinSequence of NAT st p in dom T1 holds T1 . p = T2 . p ; ::_thesis: T1 = T2 now__::_thesis:_for_x_being_set_st_x_in_dom_T1_holds_ T1_._x_=_T2_._x let x be set ; ::_thesis: ( x in dom T1 implies T1 . x = T2 . x ) assume x in dom T1 ; ::_thesis: T1 . x = T2 . x then reconsider p = x as Element of dom T1 ; T1 . p = T2 . p by A2; hence T1 . x = T2 . x ; ::_thesis: verum end; hence T1 = T2 by A1, FUNCT_1:2; ::_thesis: verum end; scheme :: TREES_2:sch 6 DTreeEx{ F1() -> Tree, P1[ set , set ] } : ex T being DecoratedTree st ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds P1[p,T . p] ) ) provided A1: for p being FinSequence of NAT st p in F1() holds ex x being set st P1[p,x] proof A2: for x being set st x in F1() holds ex y being set st P1[x,y] proof let x be set ; ::_thesis: ( x in F1() implies ex y being set st P1[x,y] ) assume x in F1() ; ::_thesis: ex y being set st P1[x,y] then reconsider p = x as Element of F1() ; ex y being set st P1[p,y] by A1; hence ex y being set st P1[x,y] ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = F1() & ( for x being set st x in F1() holds P1[x,f . x] ) ) from CLASSES1:sch_1(A2); reconsider T = f as DecoratedTree by A3, Def8; take T ; ::_thesis: ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds P1[p,T . p] ) ) thus ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds P1[p,T . p] ) ) by A3; ::_thesis: verum end; scheme :: TREES_2:sch 7 DTreeLambda{ F1() -> Tree, F2( set ) -> set } : ex T being DecoratedTree st ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds T . p = F2(p) ) ) proof consider f being Function such that A1: ( dom f = F1() & ( for x being set st x in F1() holds f . x = F2(x) ) ) from FUNCT_1:sch_3(); reconsider T = f as DecoratedTree by A1, Def8; take T ; ::_thesis: ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds T . p = F2(p) ) ) thus ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds T . p = F2(p) ) ) by A1; ::_thesis: verum end; definition let T be DecoratedTree; func Leaves T -> set equals :: TREES_2:def 9 T .: (Leaves (dom T)); correctness coherence T .: (Leaves (dom T)) is set ; ; let p be FinSequence of NAT ; funcT | p -> DecoratedTree means :Def10: :: TREES_2:def 10 ( dom it = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds it . q = T . (p ^ q) ) ); existence ex b1 being DecoratedTree st ( dom b1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds b1 . q = T . (p ^ q) ) ) proof deffunc H1( FinSequence) -> set = T . (p ^ $1); thus ex t being DecoratedTree st ( dom t = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds t . q = H1(q) ) ) from TREES_2:sch_7(); ::_thesis: verum end; uniqueness for b1, b2 being DecoratedTree st dom b1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds b1 . q = T . (p ^ q) ) & dom b2 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds b2 . q = T . (p ^ q) ) holds b1 = b2 proof let T1, T2 be DecoratedTree; ::_thesis: ( dom T1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds T1 . q = T . (p ^ q) ) & dom T2 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds T2 . q = T . (p ^ q) ) implies T1 = T2 ) assume that A1: dom T1 = (dom T) | p and A2: for q being FinSequence of NAT st q in (dom T) | p holds T1 . q = T . (p ^ q) and A3: dom T2 = (dom T) | p and A4: for q being FinSequence of NAT st q in (dom T) | p holds T2 . q = T . (p ^ q) ; ::_thesis: T1 = T2 now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_(dom_T)_|_p_holds_ T1_._q_=_T2_._q let q be FinSequence of NAT ; ::_thesis: ( q in (dom T) | p implies T1 . q = T2 . q ) assume A5: q in (dom T) | p ; ::_thesis: T1 . q = T2 . q then T1 . q = T . (p ^ q) by A2; hence T1 . q = T2 . q by A4, A5; ::_thesis: verum end; hence T1 = T2 by A1, A3, Th31; ::_thesis: verum end; end; :: deftheorem defines Leaves TREES_2:def_9_:_ for T being DecoratedTree holds Leaves T = T .: (Leaves (dom T)); :: deftheorem Def10 defines | TREES_2:def_10_:_ for T being DecoratedTree for p being FinSequence of NAT for b3 being DecoratedTree holds ( b3 = T | p iff ( dom b3 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds b3 . q = T . (p ^ q) ) ) ); theorem Th32: :: TREES_2:32 for p being FinSequence of NAT for T being DecoratedTree st p in dom T holds rng (T | p) c= rng T proof let p be FinSequence of NAT ; ::_thesis: for T being DecoratedTree st p in dom T holds rng (T | p) c= rng T let T be DecoratedTree; ::_thesis: ( p in dom T implies rng (T | p) c= rng T ) assume A1: p in dom T ; ::_thesis: rng (T | p) c= rng T let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (T | p) or x in rng T ) assume x in rng (T | p) ; ::_thesis: x in rng T then consider y being set such that A2: y in dom (T | p) and A3: x = (T | p) . y by FUNCT_1:def_3; reconsider y = y as Element of dom (T | p) by A2; A4: dom (T | p) = (dom T) | p by Def10; then A5: p ^ y in dom T by A1, TREES_1:def_6; x = T . (p ^ y) by A3, A4, Def10; hence x in rng T by A5, FUNCT_1:def_3; ::_thesis: verum end; definition let D be non empty set ; let T be DecoratedTree of D; :: original: Leaves redefine func Leaves T -> Subset of D; coherence Leaves T is Subset of D proof ( T .: (Leaves (dom T)) c= rng T & rng T c= D ) by RELAT_1:111; hence Leaves T is Subset of D by XBOOLE_1:1; ::_thesis: verum end; end; registration let D be non empty set ; let T be DecoratedTree of D; let p be Element of dom T; clusterT | p -> D -valued ; coherence T | p is D -valued proof ( rng (T | p) c= rng T & rng T c= D ) by Th32; then rng (T | p) c= D by XBOOLE_1:1; hence T | p is D -valued by RELAT_1:def_19; ::_thesis: verum end; end; definition let T be DecoratedTree; let p be FinSequence of NAT ; let T1 be DecoratedTree; assume A1: p in dom T ; funcT with-replacement (p,T1) -> DecoratedTree means :: TREES_2:def 11 ( dom it = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & it . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) ); existence ex b1 being DecoratedTree st ( dom b1 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b1 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) ) proof defpred S1[ FinSequence, set ] means ( ( not p is_a_prefix_of $1 & $2 = T . $1 ) or ex r being FinSequence of NAT st ( r in dom T1 & $1 = p ^ r & $2 = T1 . r ) ); A2: for q being FinSequence of NAT st q in (dom T) with-replacement (p,(dom T1)) holds ex x being set st S1[q,x] proof let q be FinSequence of NAT ; ::_thesis: ( q in (dom T) with-replacement (p,(dom T1)) implies ex x being set st S1[q,x] ) assume A3: q in (dom T) with-replacement (p,(dom T1)) ; ::_thesis: ex x being set st S1[q,x] now__::_thesis:_ex_x_being_set_st_S1[q,x] percases ( p is_a_proper_prefix_of q or p = q or not p is_a_prefix_of q ) by XBOOLE_0:def_8; suppose p is_a_proper_prefix_of q ; ::_thesis: ex x being set st S1[q,x] then consider r being FinSequence of NAT such that A4: ( r in dom T1 & q = p ^ r ) by A1, A3, TREES_1:def_9; thus ex x being set st S1[q,x] ::_thesis: verum proof take T1 . r ; ::_thesis: S1[q,T1 . r] thus S1[q,T1 . r] by A4; ::_thesis: verum end; end; supposeA5: p = q ; ::_thesis: ex x being set st S1[q,x] thus ex x being set st S1[q,x] ::_thesis: verum proof take T1 . ({} NAT) ; ::_thesis: S1[q,T1 . ({} NAT)] ( {} NAT in dom T1 & q = p ^ (<*> NAT) ) by A5, FINSEQ_1:34, TREES_1:22; hence S1[q,T1 . ({} NAT)] ; ::_thesis: verum end; end; suppose not p is_a_prefix_of q ; ::_thesis: ex x being set st S1[q,x] hence ex x being set st S1[q,x] ; ::_thesis: verum end; end; end; hence ex x being set st S1[q,x] ; ::_thesis: verum end; thus ex TT being DecoratedTree st ( dom TT = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT st q in (dom T) with-replacement (p,(dom T1)) holds S1[q,TT . q] ) ) from TREES_2:sch_6(A2); ::_thesis: verum end; uniqueness for b1, b2 being DecoratedTree st dom b1 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b1 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b2 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds b1 = b2 proof let D1, D2 be DecoratedTree; ::_thesis: ( dom D1 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 ) assume that A6: dom D1 = (dom T) with-replacement (p,(dom T1)) and A7: for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) and A8: dom D2 = (dom T) with-replacement (p,(dom T1)) and A9: for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ; ::_thesis: D1 = D2 now__::_thesis:_for_q_being_FinSequence_of_NAT_st_q_in_dom_D1_holds_ not_D1_._q_<>_D2_._q let q be FinSequence of NAT ; ::_thesis: ( q in dom D1 implies not D1 . q <> D2 . q ) assume that A10: q in dom D1 and A11: D1 . q <> D2 . q ; ::_thesis: contradiction A12: ( ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) by A6, A7, A10; ( ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A6, A9, A10; hence contradiction by A11, A12, FINSEQ_1:33, TREES_1:1; ::_thesis: verum end; hence D1 = D2 by A6, A8, Th31; ::_thesis: verum end; end; :: deftheorem defines with-replacement TREES_2:def_11_:_ for T being DecoratedTree for p being FinSequence of NAT for T1 being DecoratedTree st p in dom T holds for b4 being DecoratedTree holds ( b4 = T with-replacement (p,T1) iff ( dom b4 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds ( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & b4 . q = T . q ) or ex r being FinSequence of NAT st ( r in dom T1 & q = p ^ r & b4 . q = T1 . r ) ) ) ) ); registration let W be Tree; let x be set ; clusterW --> x -> DecoratedTree-like ; coherence W --> x is DecoratedTree-like proof dom (W --> x) = W by FUNCOP_1:13; hence W --> x is DecoratedTree-like by Def8; ::_thesis: verum end; end; theorem Th33: :: TREES_2:33 for D being non empty set st ( for x being set st x in D holds x is Tree ) holds union D is Tree proof let D be non empty set ; ::_thesis: ( ( for x being set st x in D holds x is Tree ) implies union D is Tree ) assume A1: for x being set st x in D holds x is Tree ; ::_thesis: union D is Tree then reconsider x = the Element of D as Tree ; x c= union D by ZFMISC_1:74; then reconsider T = union D as non empty set ; T is Tree-like proof for X being set st X in D holds X c= NAT * proof let X be set ; ::_thesis: ( X in D implies X c= NAT * ) assume X in D ; ::_thesis: X c= NAT * then X is Tree by A1; hence X c= NAT * by TREES_1:def_3; ::_thesis: verum end; hence T c= NAT * by ZFMISC_1:76; :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds ( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) ) thus for p being FinSequence of NAT st p in T holds ProperPrefixes p c= T ::_thesis: for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) proof let p be FinSequence of NAT ; ::_thesis: ( p in T implies ProperPrefixes p c= T ) assume p in T ; ::_thesis: ProperPrefixes p c= T then consider X being set such that A2: p in X and A3: X in D by TARSKI:def_4; reconsider X = X as Tree by A1, A3; ( ProperPrefixes p c= X & X c= T ) by A2, A3, TREES_1:def_3, ZFMISC_1:74; hence ProperPrefixes p c= T by XBOOLE_1:1; ::_thesis: verum end; let p be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds ( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> in T ) let k, n be Element of NAT ; ::_thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T ) assume that A4: p ^ <*k*> in T and A5: n <= k ; ::_thesis: p ^ <*n*> in T consider X being set such that A6: p ^ <*k*> in X and A7: X in D by A4, TARSKI:def_4; reconsider X = X as Tree by A1, A7; p ^ <*n*> in X by A5, A6, TREES_1:def_3; hence p ^ <*n*> in T by A7, TARSKI:def_4; ::_thesis: verum end; hence union D is Tree ; ::_thesis: verum end; theorem Th34: :: TREES_2:34 for X being set st ( for x being set st x in X holds x is Function ) & X is c=-linear holds ( union X is Relation-like & union X is Function-like ) proof let X be set ; ::_thesis: ( ( for x being set st x in X holds x is Function ) & X is c=-linear implies ( union X is Relation-like & union X is Function-like ) ) assume that A1: for x being set st x in X holds x is Function and A2: X is c=-linear ; ::_thesis: ( union X is Relation-like & union X is Function-like ) thus for a being set st a in union X holds ex b, c being set st [b,c] = a :: according to RELAT_1:def_1 ::_thesis: union X is Function-like proof let a be set ; ::_thesis: ( a in union X implies ex b, c being set st [b,c] = a ) assume a in union X ; ::_thesis: ex b, c being set st [b,c] = a then consider x being set such that A3: a in x and A4: x in X by TARSKI:def_4; reconsider x = x as Function by A1, A4; x = x ; hence ex b, c being set st [b,c] = a by A3, RELAT_1:def_1; ::_thesis: verum end; let a be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being set holds ( not [a,b1] in union X or not [a,b2] in union X or b1 = b2 ) let b, c be set ; ::_thesis: ( not [a,b] in union X or not [a,c] in union X or b = c ) assume that A5: [a,b] in union X and A6: [a,c] in union X ; ::_thesis: b = c consider x being set such that A7: [a,b] in x and A8: x in X by A5, TARSKI:def_4; consider y being set such that A9: [a,c] in y and A10: y in X by A6, TARSKI:def_4; reconsider x = x as Function by A1, A8; reconsider y = y as Function by A1, A10; x,y are_c=-comparable by A2, A8, A10, ORDINAL1:def_8; then ( x c= y or y c= x ) by XBOOLE_0:def_9; hence b = c by A7, A9, FUNCT_1:def_1; ::_thesis: verum end; theorem Th35: :: TREES_2:35 for D being non empty set st ( for x being set st x in D holds x is DecoratedTree ) & D is c=-linear holds union D is DecoratedTree proof let D be non empty set ; ::_thesis: ( ( for x being set st x in D holds x is DecoratedTree ) & D is c=-linear implies union D is DecoratedTree ) assume that A1: for x being set st x in D holds x is DecoratedTree and A2: D is c=-linear ; ::_thesis: union D is DecoratedTree for x being set st x in D holds x is Function by A1; then reconsider T = union D as Function by A2, Th34; defpred S1[ set , set ] means ex T1 being DecoratedTree st ( $1 = T1 & dom T1 = $2 ); A3: for x being set st x in D holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in D implies ex y being set st S1[x,y] ) assume x in D ; ::_thesis: ex y being set st S1[x,y] then reconsider T1 = x as DecoratedTree by A1; dom T1 = dom T1 ; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A4: ( dom f = D & ( for x being set st x in D holds S1[x,f . x] ) ) from CLASSES1:sch_1(A3); reconsider E = rng f as non empty set by A4, RELAT_1:42; now__::_thesis:_for_x_being_set_st_x_in_E_holds_ x_is_Tree let x be set ; ::_thesis: ( x in E implies x is Tree ) assume x in E ; ::_thesis: x is Tree then consider y being set such that A5: ( y in dom f & x = f . y ) by FUNCT_1:def_3; ex T1 being DecoratedTree st ( y = T1 & dom T1 = x ) by A4, A5; hence x is Tree ; ::_thesis: verum end; then A6: union E is Tree by Th33; dom T = union E proof thus dom T c= union E :: according to XBOOLE_0:def_10 ::_thesis: union E c= dom T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom T or x in union E ) assume x in dom T ; ::_thesis: x in union E then consider y being set such that A7: [x,y] in T by XTUPLE_0:def_12; consider X being set such that A8: [x,y] in X and A9: X in D by A7, TARSKI:def_4; consider T1 being DecoratedTree such that A10: X = T1 and A11: dom T1 = f . X by A4, A9; A12: dom T1 in rng f by A4, A9, A11, FUNCT_1:def_3; A13: x in dom T1 by A8, A10, XTUPLE_0:def_12; dom T1 c= union E by A12, ZFMISC_1:74; hence x in union E by A13; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union E or x in dom T ) assume x in union E ; ::_thesis: x in dom T then consider X being set such that A14: x in X and A15: X in E by TARSKI:def_4; consider y being set such that A16: y in dom f and A17: X = f . y by A15, FUNCT_1:def_3; consider T1 being DecoratedTree such that A18: y = T1 and A19: dom T1 = X by A4, A16, A17; [x,(T1 . x)] in T1 by A14, A19, FUNCT_1:1; then [x,(T1 . x)] in union D by A4, A16, A18, TARSKI:def_4; hence x in dom T by XTUPLE_0:def_12; ::_thesis: verum end; hence union D is DecoratedTree by A6, Def8; ::_thesis: verum end; theorem Th36: :: TREES_2:36 for D9, D being non empty set st ( for x being set st x in D9 holds x is DecoratedTree of D ) & D9 is c=-linear holds union D9 is DecoratedTree of D proof let D9, D be non empty set ; ::_thesis: ( ( for x being set st x in D9 holds x is DecoratedTree of D ) & D9 is c=-linear implies union D9 is DecoratedTree of D ) assume that A1: for x being set st x in D9 holds x is DecoratedTree of D and A2: D9 is c=-linear ; ::_thesis: union D9 is DecoratedTree of D for x being set st x in D9 holds x is DecoratedTree by A1; then reconsider T = union D9 as DecoratedTree by A2, Th35; rng T c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng T or x in D ) assume x in rng T ; ::_thesis: x in D then consider y being set such that A3: ( y in dom T & x = T . y ) by FUNCT_1:def_3; [y,x] in T by A3, FUNCT_1:1; then consider X being set such that A4: [y,x] in X and A5: X in D9 by TARSKI:def_4; reconsider X = X as DecoratedTree of D by A1, A5; ( y in dom X & x = X . y ) by A4, FUNCT_1:1; then A6: x in rng X by FUNCT_1:def_3; thus x in D by A6; ::_thesis: verum end; hence union D9 is DecoratedTree of D by RELAT_1:def_19; ::_thesis: verum end; scheme :: TREES_2:sch 8 DTreeStructEx{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> set , F4() -> Function of [:F1(),NAT:],F1() } : ex T being DecoratedTree of F1() st ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) provided A1: for d being Element of F1() for k1, k2 being Element of NAT st k1 <= k2 & k2 in F3(d) holds k1 in F3(d) proof defpred S1[ Element of NAT ] means ex T being DecoratedTree of F1() st ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= $1 & ( len t < $1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ); A2: S1[ 0 ] proof reconsider W = {{}} as Tree ; take T = W --> F2(); ::_thesis: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) {} in W by TREES_1:22; hence T . {} = F2() by FUNCOP_1:7; ::_thesis: for t being Element of dom T holds ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) let t be Element of dom T; ::_thesis: ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) dom T = W by FUNCOP_1:13; then t = {} by TARSKI:def_1; hence len t <= 0 ; ::_thesis: ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) assume len t < 0 ; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) hence ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ; ::_thesis: verum end; 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] ) given T being DecoratedTree of F1() such that A4: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*m*>) where m is Element of NAT : m in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) ; ::_thesis: S1[k + 1] reconsider M = { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F3((T . t)) } \/ (dom T) as non empty set ; M is Tree-like proof thus M c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds ( not b1 in M or ProperPrefixes b1 c= M ) ) & ( for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M ) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in NAT * ) assume x in M ; ::_thesis: x in NAT * then A5: ( x in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F3((T . t)) } or ( x in dom T & dom T c= NAT * ) ) by TREES_1:def_3, XBOOLE_0:def_3; assume A6: not x in NAT * ; ::_thesis: contradiction then ex n being Element of NAT ex t being Element of dom T st ( x = t ^ <*n*> & n in F3((T . t)) ) by A5; hence contradiction by A6, FINSEQ_1:def_11; ::_thesis: verum end; thus for p being FinSequence of NAT st p in M holds ProperPrefixes p c= M ::_thesis: for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M ) proof let p be FinSequence of NAT ; ::_thesis: ( p in M implies ProperPrefixes p c= M ) assume p in M ; ::_thesis: ProperPrefixes p c= M then A7: ( p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F3((T . t)) } or p in dom T ) by XBOOLE_0:def_3; now__::_thesis:_(_p_in__{__(t_^_<*n*>)_where_n_is_Element_of_NAT_,_t_is_Element_of_dom_T_:_n_in_F3((T_._t))__}__implies_ProperPrefixes_p_c=_M_) assume p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F3((T . t)) } ; ::_thesis: ProperPrefixes p c= M then consider n being Element of NAT , t being Element of dom T such that A8: p = t ^ <*n*> and n in F3((T . t)) ; A9: ProperPrefixes t c= dom T by TREES_1:def_3; A10: dom T c= M by XBOOLE_1:7; A11: t in dom T ; A12: ProperPrefixes t c= M by A9, A10, XBOOLE_1:1; A13: {t} c= M by A10, A11, ZFMISC_1:31; ProperPrefixes p = (ProperPrefixes t) \/ {t} by A8, Th4; hence ProperPrefixes p c= M by A12, A13, XBOOLE_1:8; ::_thesis: verum end; then ( ProperPrefixes p c= M or ( ProperPrefixes p c= dom T & dom T c= M ) ) by A7, TREES_1:def_3, XBOOLE_1:7; hence ProperPrefixes p c= M by XBOOLE_1:1; ::_thesis: verum end; let p be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds ( not p ^ <*b1*> in M or not b2 <= b1 or p ^ <*b2*> in M ) let m, n be Element of NAT ; ::_thesis: ( not p ^ <*m*> in M or not n <= m or p ^ <*n*> in M ) assume p ^ <*m*> in M ; ::_thesis: ( not n <= m or p ^ <*n*> in M ) then A14: ( p ^ <*m*> in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : l in F3((T . t)) } or p ^ <*m*> in dom T ) by XBOOLE_0:def_3; assume that A15: n <= m and A16: not p ^ <*n*> in M ; ::_thesis: contradiction not p ^ <*n*> in dom T by A16, XBOOLE_0:def_3; then consider l being Element of NAT , t being Element of dom T such that A17: p ^ <*m*> = t ^ <*l*> and A18: l in F3((T . t)) by A14, A15, TREES_1:def_3; A19: ( len (p ^ <*m*>) = (len p) + (len <*m*>) & len <*m*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; A20: ( len (t ^ <*l*>) = (len t) + (len <*l*>) & len <*l*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; A21: ( (p ^ <*m*>) . ((len p) + 1) = m & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42; then A22: p = t by A17, A19, A20, FINSEQ_1:33; n in F3((T . t)) by A1, A15, A17, A18, A19, A20, A21; then p ^ <*n*> in { (s ^ <*i*>) where i is Element of NAT , s is Element of dom T : i in F3((T . s)) } by A22; hence contradiction by A16, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider M = M as Tree ; defpred S2[ FinSequence, set ] means ( ( $1 in dom T & $2 = T . $1 ) or ( not $1 in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( $1 = q ^ <*n*> & $2 = F4() . ((T . q),n) ) ) ); A23: for p being FinSequence of NAT st p in M holds ex x being set st S2[p,x] proof let p be FinSequence of NAT ; ::_thesis: ( p in M implies ex x being set st S2[p,x] ) assume p in M ; ::_thesis: ex x being set st S2[p,x] then A24: ( p in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : l in F3((T . t)) } or p in dom T ) by XBOOLE_0:def_3; now__::_thesis:_(_not_p_in_dom_T_implies_ex_x_being_Element_of_F1()_st_ (_(_p_in_dom_T_&_x_=_T_._p_)_or_(_not_p_in_dom_T_&_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_of_NAT_st_ (_p_=_q_^_<*n*>_&_x_=_F4()_._((T_._q),n)_)_)_)_) assume A25: not p in dom T ; ::_thesis: ex x being Element of F1() st ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F4() . ((T . q),n) ) ) ) then consider l being Element of NAT , t being Element of dom T such that A26: p = t ^ <*l*> and l in F3((T . t)) by A24; take x = F4() . ((T . t),l); ::_thesis: ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F4() . ((T . q),n) ) ) ) thus ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F4() . ((T . q),n) ) ) ) by A25, A26; ::_thesis: verum end; hence ex x being set st S2[p,x] ; ::_thesis: verum end; consider T9 being DecoratedTree such that A27: ( dom T9 = M & ( for p being FinSequence of NAT st p in M holds S2[p,T9 . p] ) ) from TREES_2:sch_6(A23); rng T9 c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng T9 or x in F1() ) assume x in rng T9 ; ::_thesis: x in F1() then consider y being set such that A28: y in dom T9 and A29: x = T9 . y by FUNCT_1:def_3; reconsider y = y as Element of dom T9 by A28; A30: now__::_thesis:_(_y_in_dom_T_implies_x_in_F1()_) assume y in dom T ; ::_thesis: x in F1() then reconsider t = y as Element of dom T ; T . t in F1() ; hence x in F1() by A27, A29; ::_thesis: verum end; now__::_thesis:_(_not_y_in_dom_T_implies_x_in_F1()_) assume A31: not y in dom T ; ::_thesis: x in F1() then consider n being Element of NAT , q being FinSequence of NAT such that A32: y = q ^ <*n*> and A33: T9 . y = F4() . ((T . q),n) by A27; y in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : l in F3((T . t)) } by A27, A31, XBOOLE_0:def_3; then consider l being Element of NAT , t being Element of dom T such that A34: y = t ^ <*l*> and l in F3((T . t)) ; A35: len <*n*> = 1 by FINSEQ_1:39; A36: len <*l*> = 1 by FINSEQ_1:39; A37: len (q ^ <*n*>) = (len q) + 1 by A35, FINSEQ_1:22; A38: len (t ^ <*l*>) = (len t) + 1 by A36, FINSEQ_1:22; ( (q ^ <*n*>) . ((len q) + 1) = n & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42; then A39: q = t by A32, A34, A37, A38, FINSEQ_1:33; T . t in F1() ; then [(T . q),n] in [:F1(),NAT:] by A39, ZFMISC_1:87; hence x in F1() by A29, A33, FUNCT_2:5; ::_thesis: verum end; hence x in F1() by A30; ::_thesis: verum end; then reconsider T9 = T9 as DecoratedTree of F1() by RELAT_1:def_19; take T9 ; ::_thesis: ( T9 . {} = F2() & ( for t being Element of dom T9 holds ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) ( <*> NAT in M & <*> NAT in dom T ) by TREES_1:22; hence T9 . {} = F2() by A4, A27; ::_thesis: for t being Element of dom T9 holds ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) let t be Element of dom T9; ::_thesis: ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) A40: now__::_thesis:_(_t_in__{__(s_^_<*l*>)_where_l_is_Element_of_NAT_,_s_is_Element_of_dom_T_:_l_in_F3((T_._s))__}__implies_len_t_<=_k_+_1_) assume t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F3((T . s)) } ; ::_thesis: len t <= k + 1 then consider l being Element of NAT , s being Element of dom T such that A41: t = s ^ <*l*> and l in F3((T . s)) ; len s <= k by A4; then ( len <*l*> = 1 & (len s) + 1 <= k + 1 ) by FINSEQ_1:39, XREAL_1:7; hence len t <= k + 1 by A41, FINSEQ_1:22; ::_thesis: verum end; now__::_thesis:_(_t_in_dom_T_implies_len_t_<=_k_+_1_) assume t in dom T ; ::_thesis: len t <= k + 1 then reconsider s = t as Element of dom T ; ( len s <= k & k <= k + 1 ) by A4, NAT_1:11; hence len t <= k + 1 by XXREAL_0:2; ::_thesis: verum end; hence len t <= k + 1 by A27, A40, XBOOLE_0:def_3; ::_thesis: ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) assume A42: len t < k + 1 ; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) A43: now__::_thesis:_t_in_dom_T assume A44: not t in dom T ; ::_thesis: contradiction then t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F3((T . s)) } by A27, XBOOLE_0:def_3; then consider l being Element of NAT , s being Element of dom T such that A45: t = s ^ <*l*> and A46: l in F3((T . s)) ; A47: len t = (len s) + (len <*l*>) by A45, FINSEQ_1:22; ( len <*l*> = 1 & len t <= k ) by A42, FINSEQ_1:39, NAT_1:13; then len s < k by A47, NAT_1:13; then succ s = { (s ^ <*m*>) where m is Element of NAT : m in F3((T . s)) } by A4; then t in succ s by A45, A46; hence contradiction by A44; ::_thesis: verum end; then A48: T9 . t = T . t by A27; reconsider t9 = t as Element of dom T by A43; thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } :: according to XBOOLE_0:def_10 ::_thesis: ( { (t ^ <*k*>) where k is Element of NAT : k in F3((T9 . t)) } c= succ t & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } ) assume x in succ t ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } then consider n being Element of NAT such that A49: x = t ^ <*n*> and A50: t ^ <*n*> in dom T9 ; now__::_thesis:_x_in__{__(t_^_<*i*>)_where_i_is_Element_of_NAT_:_i_in_F3((T9_._t))__}_ percases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ; supposeA51: t ^ <*n*> in dom T ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } then reconsider s = t ^ <*n*>, t9 = t as Element of dom T by TREES_1:21; ( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16; then len t < k by NAT_1:13; then succ t9 = { (t9 ^ <*m*>) where m is Element of NAT : m in F3((T . t9)) } by A4; hence x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } by A48, A49, A51; ::_thesis: verum end; suppose not t ^ <*n*> in dom T ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } then t ^ <*n*> in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F3((T . s)) } by A27, A50, XBOOLE_0:def_3; then consider l being Element of NAT , s being Element of dom T such that A52: t ^ <*n*> = s ^ <*l*> and A53: l in F3((T . s)) ; t = s by A52, FINSEQ_2:17; hence x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } by A48, A49, A52, A53; ::_thesis: verum end; end; end; hence x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } ; ::_thesis: verum end; thus A54: { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } c= succ t ::_thesis: for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } or x in succ t ) assume x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } ; ::_thesis: x in succ t then consider n being Element of NAT such that A55: x = t ^ <*n*> and A56: n in F3((T9 . t)) ; x = t9 ^ <*n*> by A55; then x in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F3((T . s)) } by A48, A56; then x in dom T9 by A27, XBOOLE_0:def_3; hence x in succ t by A55; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) let x be set ; ::_thesis: ( x = T9 . t & n in F3(x) implies T9 . (t ^ <*n*>) = F4() . (x,n) ) assume that A57: x = T9 . t and A58: n in F3(x) ; ::_thesis: T9 . (t ^ <*n*>) = F4() . (x,n) t ^ <*n*> in { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } by A57, A58; then A59: t ^ <*n*> in succ t by A54; now__::_thesis:_T9_._(t_^_<*n*>)_=_F4()_._(x,n) percases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ; supposeA60: t ^ <*n*> in dom T ; ::_thesis: T9 . (t ^ <*n*>) = F4() . (x,n) then reconsider s = t ^ <*n*> as Element of dom T ; ( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16; then len t9 < k by NAT_1:13; then T . (t9 ^ <*n*>) = F4() . (x,n) by A4, A48, A57, A58; hence T9 . (t ^ <*n*>) = F4() . (x,n) by A27, A59, A60; ::_thesis: verum end; suppose not t ^ <*n*> in dom T ; ::_thesis: T9 . (t ^ <*n*>) = F4() . (x,n) then consider l being Element of NAT , q being FinSequence of NAT such that A61: t ^ <*n*> = q ^ <*l*> and A62: T9 . (t ^ <*n*>) = F4() . ((T . q),l) by A27, A59; ( t = q & n = l ) by A61, FINSEQ_2:17; hence T9 . (t ^ <*n*>) = F4() . (x,n) by A27, A43, A57, A62; ::_thesis: verum end; end; end; hence T9 . (t ^ <*n*>) = F4() . (x,n) ; ::_thesis: verum end; A63: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A3); defpred S2[ set , set ] means ex T being DecoratedTree of F1() ex k being Element of NAT st ( $1 = k & $2 = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ); A64: for x being set st x in NAT holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S2[x,y] then reconsider n = x as Element of NAT ; consider T being DecoratedTree of F1() such that A65: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A63; reconsider y = T as set ; take y ; ::_thesis: S2[x,y] take T ; ::_thesis: ex k being Element of NAT st ( x = k & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) take n ; ::_thesis: ( x = n & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) thus ( x = n & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A65; ::_thesis: verum end; consider f being Function such that A66: ( dom f = NAT & ( for x being set st x in NAT holds S2[x,f . x] ) ) from CLASSES1:sch_1(A64); reconsider E = rng f as non empty set by A66, RELAT_1:42; A67: for x being set st x in E holds x is DecoratedTree of F1() proof let x be set ; ::_thesis: ( x in E implies x is DecoratedTree of F1() ) assume x in E ; ::_thesis: x is DecoratedTree of F1() then consider y being set such that A68: y in dom f and A69: x = f . y by FUNCT_1:def_3; ex T being DecoratedTree of F1() ex k being Element of NAT st ( y = k & f . y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } & ( for n being Element of NAT for x being set st x = T . t & n in F3(x) holds T . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66, A68; hence x is DecoratedTree of F1() by A69; ::_thesis: verum end; A70: for T1, T2 being DecoratedTree for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds T1 c= T2 proof let T1, T2 be DecoratedTree; ::_thesis: for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds T1 c= T2 let x, y be Element of NAT ; ::_thesis: ( T1 = f . x & T2 = f . y & x <= y implies T1 c= T2 ) assume that A71: T1 = f . x and A72: T2 = f . y and A73: x <= y ; ::_thesis: T1 c= T2 consider T19 being DecoratedTree of F1(), k1 being Element of NAT such that A74: ( x = k1 & f . x = T19 & T19 . {} = F2() & ( for t being Element of dom T19 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T19 . t)) } & ( for n being Element of NAT for x being set st x = T19 . t & n in F3(x) holds T19 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66; consider T29 being DecoratedTree of F1(), k2 being Element of NAT such that A75: ( y = k2 & f . y = T29 & T29 . {} = F2() & ( for t being Element of dom T29 holds ( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T29 . t)) } & ( for n being Element of NAT for x being set st x = T29 . t & n in F3(x) holds T29 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66; defpred S3[ Element of NAT ] means for t being Element of dom T1 st len t <= $1 holds ( t in dom T2 & T1 . t = T2 . t ); A76: S3[ 0 ] proof let t be Element of dom T1; ::_thesis: ( len t <= 0 implies ( t in dom T2 & T1 . t = T2 . t ) ) assume A77: len t <= 0 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) t = {} by A77; hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, TREES_1:22; ::_thesis: verum end; A78: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) assume A79: for t being Element of dom T1 st len t <= k holds ( t in dom T2 & T1 . t = T2 . t ) ; ::_thesis: S3[k + 1] let t be Element of dom T1; ::_thesis: ( len t <= k + 1 implies ( t in dom T2 & T1 . t = T2 . t ) ) assume len t <= k + 1 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) then A80: ( len t <= k or len t = k + 1 ) by NAT_1:8; now__::_thesis:_(_len_t_=_k_+_1_implies_(_t_in_dom_T2_&_T1_._t_=_T2_._t_)_) assume A81: len t = k + 1 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) reconsider p = t | (Seg k) as FinSequence of NAT by FINSEQ_1:18; p is_a_prefix_of t by TREES_1:def_1; then reconsider p = p as Element of dom T1 by TREES_1:20; A82: k <= k + 1 by NAT_1:11; A83: k + 1 <= k1 by A71, A74, A81; A84: len p = k by A81, A82, FINSEQ_1:17; A85: k < k1 by A83, NAT_1:13; A86: T1 . p = T2 . p by A79, A84; reconsider p9 = p as Element of dom T2 by A79, A84; t <> {} by A81; then consider q being FinSequence, x being set such that A87: t = q ^ <*x*> by FINSEQ_1:46; A88: ( p is_a_prefix_of t & q is_a_prefix_of t ) by A87, TREES_1:1, TREES_1:def_1; k + 1 = (len q) + 1 by A81, A87, FINSEQ_2:16; then A89: p = q by A84, A88, Th1, TREES_1:4; <*x*> is FinSequence of NAT by A87, FINSEQ_1:36; then A90: rng <*x*> c= NAT by FINSEQ_1:def_4; ( rng <*x*> = {x} & x in {x} ) by FINSEQ_1:38, TARSKI:def_1; then reconsider x = x as Element of NAT by A90; A91: p ^ <*x*> in succ p by A87, A89; succ p = { (p ^ <*i*>) where i is Element of NAT : i in F3((T1 . p)) } by A71, A74, A84, A85; then consider i being Element of NAT such that A92: p ^ <*x*> = p ^ <*i*> and A93: i in F3((T1 . p)) by A91; A94: k < k2 by A73, A74, A75, A85, XXREAL_0:2; then A95: succ p9 = { (p9 ^ <*l*>) where l is Element of NAT : l in F3((T2 . p9)) } by A72, A75, A84; A96: x = i by A92, FINSEQ_2:17; A97: t in succ p9 by A86, A87, A89, A92, A93, A95; T19 . t = F4() . ((T19 . p),x) by A71, A74, A84, A85, A87, A89, A93, A96; hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, A84, A86, A87, A89, A93, A94, A96, A97; ::_thesis: verum end; hence ( t in dom T2 & T1 . t = T2 . t ) by A79, A80; ::_thesis: verum end; A98: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A76, A78); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in T2 ) assume A99: x in T1 ; ::_thesis: x in T2 then consider y, z being set such that A100: [y,z] = x by RELAT_1:def_1; A101: T1 . y = z by A99, A100, FUNCT_1:1; reconsider y = y as Element of dom T1 by A99, A100, FUNCT_1:1; len y <= len y ; then ( y in dom T2 & T1 . y = T2 . y ) by A98; hence x in T2 by A100, A101, FUNCT_1:1; ::_thesis: verum end; E is c=-linear proof let T1, T2 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not T1 in E or not T2 in E or T1,T2 are_c=-comparable ) assume A102: T1 in E ; ::_thesis: ( not T2 in E or T1,T2 are_c=-comparable ) then consider x being set such that A103: x in dom f and A104: T1 = f . x by FUNCT_1:def_3; assume A105: T2 in E ; ::_thesis: T1,T2 are_c=-comparable then consider y being set such that A106: y in dom f and A107: T2 = f . y by FUNCT_1:def_3; A108: T1 is DecoratedTree by A67, A102; A109: T2 is DecoratedTree by A67, A105; reconsider x = x, y = y as Element of NAT by A66, A103, A106; ( x <= y or y <= x ) ; hence ( T1 c= T2 or T2 c= T1 ) by A70, A104, A107, A108, A109; :: according to XBOOLE_0:def_9 ::_thesis: verum end; then reconsider T = union (rng f) as DecoratedTree of F1() by A67, Th36; take T ; ::_thesis: ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) consider T9 being DecoratedTree of F1(), k being Element of NAT such that A110: ( 0 = k & f . 0 = T9 & T9 . {} = F2() & ( for t being Element of dom T9 holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T9 . t)) } & ( for n being Element of NAT for x being set st x = T9 . t & n in F3(x) holds T9 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66; {} in dom T9 by TREES_1:22; then A111: [{},F2()] in T9 by A110, FUNCT_1:1; T9 in rng f by A66, A110, FUNCT_1:def_3; then [{},F2()] in T by A111, TARSKI:def_4; hence T . {} = F2() by FUNCT_1:1; ::_thesis: for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) A112: for T1 being DecoratedTree for x being set st T1 in E & x in dom T1 holds ( x in dom T & T1 . x = T . x ) proof let T1 be DecoratedTree; ::_thesis: for x being set st T1 in E & x in dom T1 holds ( x in dom T & T1 . x = T . x ) let x be set ; ::_thesis: ( T1 in E & x in dom T1 implies ( x in dom T & T1 . x = T . x ) ) assume that A113: T1 in E and A114: x in dom T1 ; ::_thesis: ( x in dom T & T1 . x = T . x ) [x,(T1 . x)] in T1 by A114, FUNCT_1:1; then [x,(T1 . x)] in T by A113, TARSKI:def_4; hence ( x in dom T & T1 . x = T . x ) by FUNCT_1:1; ::_thesis: verum end; let t be Element of dom T; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } & ( for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } :: according to XBOOLE_0:def_10 ::_thesis: ( { (t ^ <*k*>) where k is Element of NAT : k in F3((T . t)) } c= succ t & ( for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } ) assume x in succ t ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } then consider l being Element of NAT such that A115: x = t ^ <*l*> and A116: t ^ <*l*> in dom T ; [x,(T . x)] in T by A115, A116, FUNCT_1:1; then consider X being set such that A117: [x,(T . x)] in X and A118: X in rng f by TARSKI:def_4; consider y being set such that A119: y in NAT and A120: X = f . y by A66, A118, FUNCT_1:def_3; consider T1 being DecoratedTree of F1(), k1 being Element of NAT such that A121: ( y = k1 & f . y = T1 & T1 . {} = F2() & ( for t being Element of dom T1 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T1 . t)) } & ( for n being Element of NAT for x being set st x = T1 . t & n in F3(x) holds T1 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66, A119; A122: t ^ <*l*> in dom T1 by A115, A117, A120, A121, FUNCT_1:1; then reconsider t9 = t, p = t ^ <*l*> as Element of dom T1 by TREES_1:21; len p <= k1 by A121; then (len t) + 1 <= k1 by FINSEQ_2:16; then A123: len t9 < k1 by NAT_1:13; then A124: succ t9 = { (t9 ^ <*i*>) where i is Element of NAT : i in F3((T1 . t9)) } by A121; T1 . t = T . t by A112, A118, A120, A121, A123; hence x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } by A115, A122, A124; ::_thesis: verum end; [t,(T . t)] in T by FUNCT_1:1; then consider X being set such that A125: [t,(T . t)] in X and A126: X in E by TARSKI:def_4; consider y being set such that A127: y in NAT and A128: X = f . y by A66, A126, FUNCT_1:def_3; reconsider y = y as Element of NAT by A127; consider T1 being DecoratedTree of F1(), k1 being Element of NAT such that A129: ( y = k1 & f . y = T1 & T1 . {} = F2() & ( for t being Element of dom T1 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T1 . t)) } & ( for n being Element of NAT for x being set st x = T1 . t & n in F3(x) holds T1 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66; consider T2 being DecoratedTree of F1(), k2 being Element of NAT such that A130: ( y + 1 = k2 & f . (y + 1) = T2 & T2 . {} = F2() & ( for t being Element of dom T2 holds ( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : i in F3((T2 . t)) } & ( for n being Element of NAT for x being set st x = T2 . t & n in F3(x) holds T2 . (t ^ <*n*>) = F4() . (x,n) ) ) ) ) ) ) by A66; y <= y + 1 by NAT_1:11; then A131: T1 c= T2 by A70, A129, A130; reconsider t1 = t as Element of dom T1 by A125, A128, A129, FUNCT_1:1; A132: len t1 <= y by A129; A133: T2 . t = T . t by A125, A128, A129, A131, FUNCT_1:1; reconsider t2 = t as Element of dom T2 by A125, A128, A129, A131, FUNCT_1:1; A134: len t2 < y + 1 by A132, NAT_1:13; then A135: succ t2 = { (t2 ^ <*i*>) where i is Element of NAT : i in F3((T2 . t2)) } by A130; thus { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } c= succ t ::_thesis: for n being Element of NAT st n in F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } or x in succ t ) assume A136: x in { (t ^ <*i*>) where i is Element of NAT : i in F3((T . t)) } ; ::_thesis: x in succ t then A137: ex l being Element of NAT st ( x = t ^ <*l*> & l in F3((T . t)) ) ; A138: x in succ t2 by A130, A133, A134, A136; T2 in E by A66, A130, FUNCT_1:def_3; then x in dom T by A112, A138; hence x in succ t by A137; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( n in F3((T . t)) implies T . (t ^ <*n*>) = F4() . ((T . t),n) ) assume A139: n in F3((T . t)) ; ::_thesis: T . (t ^ <*n*>) = F4() . ((T . t),n) then A140: t ^ <*n*> in succ t2 by A133, A135; T2 in E by A66, A130, FUNCT_1:def_3; then T2 . (t ^ <*n*>) = T . (t ^ <*n*>) by A112, A140; hence T . (t ^ <*n*>) = F4() . ((T . t),n) by A130, A133, A134, A139; ::_thesis: verum end; scheme :: TREES_2:sch 9 DTreeStructFinEx{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> Element of NAT , F4() -> Function of [:F1(),NAT:],F1() } : ex T being DecoratedTree of F1() st ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } & ( for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) proof deffunc H1( Element of NAT ) -> set = { i where i is Element of NAT : i < $1 } ; deffunc H2( set ) -> set = H1(F3($1)); A1: for d being Element of F1() for k1, k2 being Element of NAT st k1 <= k2 & k2 in H2(d) holds k1 in H2(d) proof let d be Element of F1(); ::_thesis: for k1, k2 being Element of NAT st k1 <= k2 & k2 in H2(d) holds k1 in H2(d) let k1, k2 be Element of NAT ; ::_thesis: ( k1 <= k2 & k2 in H2(d) implies k1 in H2(d) ) assume A2: ( k1 <= k2 & k2 in { i where i is Element of NAT : i < F3(d) } ) ; ::_thesis: k1 in H2(d) then ex i being Element of NAT st ( k2 = i & i < F3(d) ) ; then k1 < F3(d) by A2, XXREAL_0:2; hence k1 in H2(d) ; ::_thesis: verum end; consider T being DecoratedTree of F1() such that A3: ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in H2(T . t) } & ( for n being Element of NAT st n in H2(T . t) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) from TREES_2:sch_8(A1); take T ; ::_thesis: ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } & ( for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) thus T . {} = F2() by A3; ::_thesis: for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } & ( for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) let t be Element of dom T; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } & ( for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) A4: succ t = { (t ^ <*k*>) where k is Element of NAT : k in H1(F3((T . t))) } by A3; thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } :: according to XBOOLE_0:def_10 ::_thesis: ( { (t ^ <*k*>) where k is Element of NAT : k < F3((T . t)) } c= succ t & ( for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } ) assume x in succ t ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } then consider l being Element of NAT such that A5: x = t ^ <*l*> and A6: l in H1(F3((T . t))) by A4; ex i being Element of NAT st ( l = i & i < F3((T . t)) ) by A6; hence x in { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } by A5; ::_thesis: verum end; thus { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } c= succ t ::_thesis: for n being Element of NAT st n < F3((T . t)) holds T . (t ^ <*n*>) = F4() . ((T . t),n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } or x in succ t ) assume x in { (t ^ <*i*>) where i is Element of NAT : i < F3((T . t)) } ; ::_thesis: x in succ t then consider l being Element of NAT such that A7: x = t ^ <*l*> and A8: l < F3((T . t)) ; l in H1(F3((T . t))) by A8; hence x in succ t by A4, A7; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( n < F3((T . t)) implies T . (t ^ <*n*>) = F4() . ((T . t),n) ) assume n < F3((T . t)) ; ::_thesis: T . (t ^ <*n*>) = F4() . ((T . t),n) then n in H1(F3((T . t))) ; hence T . (t ^ <*n*>) = F4() . ((T . t),n) by A3; ::_thesis: verum end; begin registration let Tr be finite Tree; let v be Element of Tr; cluster succ v -> finite ; coherence succ v is finite ; end; definition let Tr be finite Tree; let v be Element of Tr; func branchdeg v -> set equals :: TREES_2:def 12 card (succ v); correctness coherence card (succ v) is set ; ; end; :: deftheorem defines branchdeg TREES_2:def_12_:_ for Tr being finite Tree for v being Element of Tr holds branchdeg v = card (succ v); registration cluster Relation-like Function-like finite DecoratedTree-like for set ; existence ex b1 being DecoratedTree st b1 is finite proof reconsider T = {{}} as Tree ; take T --> {} ; ::_thesis: T --> {} is finite thus T --> {} is finite ; ::_thesis: verum end; end; registration let D be non empty set ; cluster Relation-like D -valued Function-like finite DecoratedTree-like for set ; existence ex b1 being DecoratedTree of D st b1 is finite proof set d = the Element of D; reconsider T = {{}} as Tree ; take T --> the Element of D ; ::_thesis: T --> the Element of D is finite thus T --> the Element of D is finite ; ::_thesis: verum end; end; registration let a, b be non empty set ; cluster Relation-like a -defined b -valued non empty for Element of bool [:a,b:]; existence not for b1 being Relation of a,b holds b1 is empty proof [:a,b:] c= [:a,b:] ; hence not for b1 being Relation of a,b holds b1 is empty ; ::_thesis: verum end; end; theorem :: TREES_2:37 for Z1, Z2 being Tree for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z2 st v = p ^ w holds succ v, succ w are_equipotent proof let Z1, Z2 be Tree; ::_thesis: for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z2 st v = p ^ w holds succ v, succ w are_equipotent let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z2 st v = p ^ w holds succ v, succ w are_equipotent ) assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z2 st v = p ^ w holds succ v, succ w are_equipotent set T = Z1 with-replacement (p,Z2); let t be Element of Z1 with-replacement (p,Z2); ::_thesis: for w being Element of Z2 st t = p ^ w holds succ t, succ w are_equipotent let t2 be Element of Z2; ::_thesis: ( t = p ^ t2 implies succ t, succ t2 are_equipotent ) assume A2: t = p ^ t2 ; ::_thesis: succ t, succ t2 are_equipotent then A3: p is_a_prefix_of t by TREES_1:1; A4: for n being Element of NAT holds ( t ^ <*n*> in Z1 with-replacement (p,Z2) iff t2 ^ <*n*> in Z2 ) proof let n be Element of NAT ; ::_thesis: ( t ^ <*n*> in Z1 with-replacement (p,Z2) iff t2 ^ <*n*> in Z2 ) A5: p is_a_proper_prefix_of t ^ <*n*> by A3, TREES_1:8; A6: t ^ <*n*> = p ^ (t2 ^ <*n*>) by A2, FINSEQ_1:32; thus ( t ^ <*n*> in Z1 with-replacement (p,Z2) implies t2 ^ <*n*> in Z2 ) ::_thesis: ( t2 ^ <*n*> in Z2 implies t ^ <*n*> in Z1 with-replacement (p,Z2) ) proof assume t ^ <*n*> in Z1 with-replacement (p,Z2) ; ::_thesis: t2 ^ <*n*> in Z2 then ex w being FinSequence of NAT st ( w in Z2 & t ^ <*n*> = p ^ w ) by A1, A5, TREES_1:def_9; hence t2 ^ <*n*> in Z2 by A6, FINSEQ_1:33; ::_thesis: verum end; assume t2 ^ <*n*> in Z2 ; ::_thesis: t ^ <*n*> in Z1 with-replacement (p,Z2) hence t ^ <*n*> in Z1 with-replacement (p,Z2) by A1, A6, TREES_1:def_9; ::_thesis: verum end; defpred S1[ set , set ] means for n being Element of NAT st $1 = t ^ <*n*> holds $2 = t2 ^ <*n*>; A7: for x being set st x in succ t holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in succ t implies ex y being set st S1[x,y] ) assume x in succ t ; ::_thesis: ex y being set st S1[x,y] then consider n being Element of NAT such that A8: x = t ^ <*n*> and t ^ <*n*> in Z1 with-replacement (p,Z2) ; take t2 ^ <*n*> ; ::_thesis: S1[x,t2 ^ <*n*>] let m be Element of NAT ; ::_thesis: ( x = t ^ <*m*> implies t2 ^ <*n*> = t2 ^ <*m*> ) assume x = t ^ <*m*> ; ::_thesis: t2 ^ <*n*> = t2 ^ <*m*> hence t2 ^ <*n*> = t2 ^ <*m*> by A8, FINSEQ_1:33; ::_thesis: verum end; consider f being Function such that A9: ( dom f = succ t & ( for x being set st x in succ t holds S1[x,f . x] ) ) from CLASSES1:sch_1(A7); now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_f_implies_x_in_succ_t2_)_&_(_x_in_succ_t2_implies_x_in_rng_f_)_) let x be set ; ::_thesis: ( ( x in rng f implies x in succ t2 ) & ( x in succ t2 implies x in rng f ) ) thus ( x in rng f implies x in succ t2 ) ::_thesis: ( x in succ t2 implies x in rng f ) proof assume x in rng f ; ::_thesis: x in succ t2 then consider y being set such that A10: y in dom f and A11: x = f . y by FUNCT_1:def_3; consider n being Element of NAT such that A12: y = t ^ <*n*> and A13: t ^ <*n*> in Z1 with-replacement (p,Z2) by A9, A10; A14: x = t2 ^ <*n*> by A9, A10, A11, A12; t2 ^ <*n*> in Z2 by A4, A13; hence x in succ t2 by A14; ::_thesis: verum end; assume x in succ t2 ; ::_thesis: x in rng f then consider n being Element of NAT such that A15: x = t2 ^ <*n*> and A16: t2 ^ <*n*> in Z2 ; t ^ <*n*> in Z1 with-replacement (p,Z2) by A4, A16; then A17: t ^ <*n*> in dom f by A9; then f . (t ^ <*n*>) = x by A9, A15; hence x in rng f by A17, FUNCT_1:def_3; ::_thesis: verum end; then A18: rng f = succ t2 by TARSKI:1; f is one-to-one proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in dom f or not b1 in dom f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A19: x1 in dom f and A20: x2 in dom f and A21: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider m being Element of NAT such that A22: x1 = t ^ <*m*> and t ^ <*m*> in Z1 with-replacement (p,Z2) by A9, A19; consider k being Element of NAT such that A23: x2 = t ^ <*k*> and t ^ <*k*> in Z1 with-replacement (p,Z2) by A9, A20; t2 ^ <*m*> = f . x1 by A9, A19, A22 .= t2 ^ <*k*> by A9, A20, A21, A23 ; hence x1 = x2 by A22, A23, FINSEQ_1:33; ::_thesis: verum end; hence succ t, succ t2 are_equipotent by A9, A18, WELLORD2:def_4; ::_thesis: verum end; scheme :: TREES_2:sch 10 DTreeStructEx{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set ], F3() -> Function of [:F1(),NAT:],F1() } : ex T being DecoratedTree of F1() st ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) ) ) provided A1: for d being Element of F1() for k1, k2 being Element of NAT st k1 <= k2 & P1[k2,d] holds P1[k1,d] proof defpred S1[ Element of NAT ] means ex T being DecoratedTree of F1() st ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= $1 & ( len t < $1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ); A2: S1[ 0 ] proof reconsider W = {{}} as Tree ; take T = W --> F2(); ::_thesis: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) {} in W by TREES_1:22; hence T . {} = F2() by FUNCOP_1:7; ::_thesis: for t being Element of dom T holds ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) let t be Element of dom T; ::_thesis: ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) dom T = W by FUNCOP_1:13; then t = {} by TARSKI:def_1; hence len t <= 0 ; ::_thesis: ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) assume len t < 0 ; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) hence ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ; ::_thesis: verum end; 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] ) given T being DecoratedTree of F1() such that A4: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*m*>) where m is Element of NAT : P1[m,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) ; ::_thesis: S1[k + 1] reconsider M = { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } \/ (dom T) as non empty set ; M is Tree-like proof thus M c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds ( not b1 in M or ProperPrefixes b1 c= M ) ) & ( for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M ) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in NAT * ) assume x in M ; ::_thesis: x in NAT * then A5: ( x in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } or ( x in dom T & dom T c= NAT * ) ) by TREES_1:def_3, XBOOLE_0:def_3; assume A6: not x in NAT * ; ::_thesis: contradiction then ex n being Element of NAT ex t being Element of dom T st ( x = t ^ <*n*> & P1[n,T . t] ) by A5; hence contradiction by A6, FINSEQ_1:def_11; ::_thesis: verum end; thus for p being FinSequence of NAT st p in M holds ProperPrefixes p c= M ::_thesis: for b1 being FinSequence of NAT for b2, b3 being Element of NAT holds ( not b1 ^ <*b2*> in M or not b3 <= b2 or b1 ^ <*b3*> in M ) proof let p be FinSequence of NAT ; ::_thesis: ( p in M implies ProperPrefixes p c= M ) assume p in M ; ::_thesis: ProperPrefixes p c= M then A7: ( p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } or p in dom T ) by XBOOLE_0:def_3; now__::_thesis:_(_p_in__{__(t_^_<*n*>)_where_n_is_Element_of_NAT_,_t_is_Element_of_dom_T_:_P1[n,T_._t]__}__implies_ProperPrefixes_p_c=_M_) assume p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : P1[n,T . t] } ; ::_thesis: ProperPrefixes p c= M then consider n being Element of NAT , t being Element of dom T such that A8: p = t ^ <*n*> and P1[n,T . t] ; A9: ProperPrefixes t c= dom T by TREES_1:def_3; A10: dom T c= M by XBOOLE_1:7; A11: t in dom T ; A12: ProperPrefixes t c= M by A9, A10, XBOOLE_1:1; A13: {t} c= M by A10, A11, ZFMISC_1:31; ProperPrefixes p = (ProperPrefixes t) \/ {t} by A8, Th4; hence ProperPrefixes p c= M by A12, A13, XBOOLE_1:8; ::_thesis: verum end; then ( ProperPrefixes p c= M or ( ProperPrefixes p c= dom T & dom T c= M ) ) by A7, TREES_1:def_3, XBOOLE_1:7; hence ProperPrefixes p c= M by XBOOLE_1:1; ::_thesis: verum end; let p be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds ( not p ^ <*b1*> in M or not b2 <= b1 or p ^ <*b2*> in M ) let m, n be Element of NAT ; ::_thesis: ( not p ^ <*m*> in M or not n <= m or p ^ <*n*> in M ) assume p ^ <*m*> in M ; ::_thesis: ( not n <= m or p ^ <*n*> in M ) then A14: ( p ^ <*m*> in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : P1[l,T . t] } or p ^ <*m*> in dom T ) by XBOOLE_0:def_3; assume that A15: n <= m and A16: not p ^ <*n*> in M ; ::_thesis: contradiction not p ^ <*n*> in dom T by A16, XBOOLE_0:def_3; then consider l being Element of NAT , t being Element of dom T such that A17: p ^ <*m*> = t ^ <*l*> and A18: P1[l,T . t] by A14, A15, TREES_1:def_3; A19: ( len (p ^ <*m*>) = (len p) + (len <*m*>) & len <*m*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; A20: ( len (t ^ <*l*>) = (len t) + (len <*l*>) & len <*l*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; A21: ( (p ^ <*m*>) . ((len p) + 1) = m & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42; then A22: p = t by A17, A19, A20, FINSEQ_1:33; P1[n,T . t] by A1, A15, A17, A18, A19, A20, A21; then p ^ <*n*> in { (s ^ <*i*>) where i is Element of NAT , s is Element of dom T : P1[i,T . s] } by A22; hence contradiction by A16, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider M = M as Tree ; defpred S2[ FinSequence, set ] means ( ( $1 in dom T & $2 = T . $1 ) or ( not $1 in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( $1 = q ^ <*n*> & $2 = F3() . ((T . q),n) ) ) ); A23: for p being FinSequence of NAT st p in M holds ex x being set st S2[p,x] proof let p be FinSequence of NAT ; ::_thesis: ( p in M implies ex x being set st S2[p,x] ) assume p in M ; ::_thesis: ex x being set st S2[p,x] then A24: ( p in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : P1[l,T . t] } or p in dom T ) by XBOOLE_0:def_3; now__::_thesis:_(_not_p_in_dom_T_implies_ex_x_being_Element_of_F1()_st_ (_(_p_in_dom_T_&_x_=_T_._p_)_or_(_not_p_in_dom_T_&_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_of_NAT_st_ (_p_=_q_^_<*n*>_&_x_=_F3()_._((T_._q),n)_)_)_)_) assume A25: not p in dom T ; ::_thesis: ex x being Element of F1() st ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F3() . ((T . q),n) ) ) ) then consider l being Element of NAT , t being Element of dom T such that A26: p = t ^ <*l*> and P1[l,T . t] by A24; take x = F3() . ((T . t),l); ::_thesis: ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F3() . ((T . q),n) ) ) ) thus ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Element of NAT ex q being FinSequence of NAT st ( p = q ^ <*n*> & x = F3() . ((T . q),n) ) ) ) by A25, A26; ::_thesis: verum end; hence ex x being set st S2[p,x] ; ::_thesis: verum end; consider T9 being DecoratedTree such that A27: ( dom T9 = M & ( for p being FinSequence of NAT st p in M holds S2[p,T9 . p] ) ) from TREES_2:sch_6(A23); rng T9 c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng T9 or x in F1() ) assume x in rng T9 ; ::_thesis: x in F1() then consider y being set such that A28: y in dom T9 and A29: x = T9 . y by FUNCT_1:def_3; reconsider y = y as Element of dom T9 by A28; A30: now__::_thesis:_(_y_in_dom_T_implies_x_in_F1()_) assume y in dom T ; ::_thesis: x in F1() then reconsider t = y as Element of dom T ; T . t in F1() ; hence x in F1() by A27, A29; ::_thesis: verum end; now__::_thesis:_(_not_y_in_dom_T_implies_x_in_F1()_) assume A31: not y in dom T ; ::_thesis: x in F1() then consider n being Element of NAT , q being FinSequence of NAT such that A32: y = q ^ <*n*> and A33: T9 . y = F3() . ((T . q),n) by A27; y in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : P1[l,T . t] } by A27, A31, XBOOLE_0:def_3; then consider l being Element of NAT , t being Element of dom T such that A34: y = t ^ <*l*> and P1[l,T . t] ; A35: len <*n*> = 1 by FINSEQ_1:39; A36: len <*l*> = 1 by FINSEQ_1:39; A37: len (q ^ <*n*>) = (len q) + 1 by A35, FINSEQ_1:22; A38: len (t ^ <*l*>) = (len t) + 1 by A36, FINSEQ_1:22; ( (q ^ <*n*>) . ((len q) + 1) = n & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42; then A39: q = t by A32, A34, A37, A38, FINSEQ_1:33; T . t in F1() ; then [(T . q),n] in [:F1(),NAT:] by A39, ZFMISC_1:87; hence x in F1() by A29, A33, FUNCT_2:5; ::_thesis: verum end; hence x in F1() by A30; ::_thesis: verum end; then reconsider T9 = T9 as DecoratedTree of F1() by RELAT_1:def_19; take T9 ; ::_thesis: ( T9 . {} = F2() & ( for t being Element of dom T9 holds ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) ( <*> NAT in M & <*> NAT in dom T ) by TREES_1:22; hence T9 . {} = F2() by A4, A27; ::_thesis: for t being Element of dom T9 holds ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) let t be Element of dom T9; ::_thesis: ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) A40: now__::_thesis:_(_t_in__{__(s_^_<*l*>)_where_l_is_Element_of_NAT_,_s_is_Element_of_dom_T_:_P1[l,T_._s]__}__implies_len_t_<=_k_+_1_) assume t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] } ; ::_thesis: len t <= k + 1 then consider l being Element of NAT , s being Element of dom T such that A41: t = s ^ <*l*> and P1[l,T . s] ; len s <= k by A4; then ( len <*l*> = 1 & (len s) + 1 <= k + 1 ) by FINSEQ_1:39, XREAL_1:7; hence len t <= k + 1 by A41, FINSEQ_1:22; ::_thesis: verum end; now__::_thesis:_(_t_in_dom_T_implies_len_t_<=_k_+_1_) assume t in dom T ; ::_thesis: len t <= k + 1 then reconsider s = t as Element of dom T ; ( len s <= k & k <= k + 1 ) by A4, NAT_1:11; hence len t <= k + 1 by XXREAL_0:2; ::_thesis: verum end; hence len t <= k + 1 by A27, A40, XBOOLE_0:def_3; ::_thesis: ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) ) assume A42: len t < k + 1 ; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) A43: now__::_thesis:_t_in_dom_T assume A44: not t in dom T ; ::_thesis: contradiction then t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] } by A27, XBOOLE_0:def_3; then consider l being Element of NAT , s being Element of dom T such that A45: t = s ^ <*l*> and A46: P1[l,T . s] ; A47: len t = (len s) + (len <*l*>) by A45, FINSEQ_1:22; ( len <*l*> = 1 & len t <= k ) by A42, FINSEQ_1:39, NAT_1:13; then len s < k by A47, NAT_1:13; then succ s = { (s ^ <*m*>) where m is Element of NAT : P1[m,T . s] } by A4; then t in succ s by A45, A46; hence contradiction by A44; ::_thesis: verum end; then A48: T9 . t = T . t by A27; reconsider t9 = t as Element of dom T by A43; thus succ t c= { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } :: according to XBOOLE_0:def_10 ::_thesis: ( { (t ^ <*k*>) where k is Element of NAT : P1[k,T9 . t] } c= succ t & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } ) assume x in succ t ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } then consider n being Element of NAT such that A49: x = t ^ <*n*> and A50: t ^ <*n*> in dom T9 ; now__::_thesis:_x_in__{__(t_^_<*i*>)_where_i_is_Element_of_NAT_:_P1[i,T9_._t]__}_ percases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ; supposeA51: t ^ <*n*> in dom T ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } then reconsider s = t ^ <*n*>, t9 = t as Element of dom T by TREES_1:21; ( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16; then len t < k by NAT_1:13; then succ t9 = { (t9 ^ <*m*>) where m is Element of NAT : P1[m,T . t9] } by A4; hence x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } by A48, A49, A51; ::_thesis: verum end; suppose not t ^ <*n*> in dom T ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } then t ^ <*n*> in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] } by A27, A50, XBOOLE_0:def_3; then consider l being Element of NAT , s being Element of dom T such that A52: t ^ <*n*> = s ^ <*l*> and A53: P1[l,T . s] ; t = s by A52, FINSEQ_2:17; hence x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } by A48, A49, A52, A53; ::_thesis: verum end; end; end; hence x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } ; ::_thesis: verum end; thus A54: { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } c= succ t ::_thesis: for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } or x in succ t ) assume x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } ; ::_thesis: x in succ t then consider n being Element of NAT such that A55: x = t ^ <*n*> and A56: P1[n,T9 . t] ; x = t9 ^ <*n*> by A55; then x in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : P1[l,T . s] } by A48, A56; then x in dom T9 by A27, XBOOLE_0:def_3; hence x in succ t by A55; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) let x be set ; ::_thesis: ( x = T9 . t & P1[n,x] implies T9 . (t ^ <*n*>) = F3() . (x,n) ) assume that A57: x = T9 . t and A58: P1[n,x] ; ::_thesis: T9 . (t ^ <*n*>) = F3() . (x,n) t ^ <*n*> in { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } by A57, A58; then A59: t ^ <*n*> in succ t by A54; now__::_thesis:_T9_._(t_^_<*n*>)_=_F3()_._(x,n) percases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ; supposeA60: t ^ <*n*> in dom T ; ::_thesis: T9 . (t ^ <*n*>) = F3() . (x,n) then reconsider s = t ^ <*n*> as Element of dom T ; ( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16; then len t9 < k by NAT_1:13; then T . (t9 ^ <*n*>) = F3() . (x,n) by A4, A48, A57, A58; hence T9 . (t ^ <*n*>) = F3() . (x,n) by A27, A59, A60; ::_thesis: verum end; suppose not t ^ <*n*> in dom T ; ::_thesis: T9 . (t ^ <*n*>) = F3() . (x,n) then consider l being Element of NAT , q being FinSequence of NAT such that A61: t ^ <*n*> = q ^ <*l*> and A62: T9 . (t ^ <*n*>) = F3() . ((T . q),l) by A27, A59; ( t = q & n = l ) by A61, FINSEQ_2:17; hence T9 . (t ^ <*n*>) = F3() . (x,n) by A27, A43, A57, A62; ::_thesis: verum end; end; end; hence T9 . (t ^ <*n*>) = F3() . (x,n) ; ::_thesis: verum end; A63: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A3); defpred S2[ set , set ] means ex T being DecoratedTree of F1() ex k being Element of NAT st ( $1 = k & $2 = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ); A64: for x being set st x in NAT holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S2[x,y] then reconsider n = x as Element of NAT ; consider T being DecoratedTree of F1() such that A65: ( T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A63; reconsider y = T as set ; take y ; ::_thesis: S2[x,y] take T ; ::_thesis: ex k being Element of NAT st ( x = k & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) take n ; ::_thesis: ( x = n & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) thus ( x = n & y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= n & ( len t < n implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A65; ::_thesis: verum end; consider f being Function such that A66: ( dom f = NAT & ( for x being set st x in NAT holds S2[x,f . x] ) ) from CLASSES1:sch_1(A64); reconsider E = rng f as non empty set by A66, RELAT_1:42; A67: for x being set st x in E holds x is DecoratedTree of F1() proof let x be set ; ::_thesis: ( x in E implies x is DecoratedTree of F1() ) assume x in E ; ::_thesis: x is DecoratedTree of F1() then consider y being set such that A68: y in dom f and A69: x = f . y by FUNCT_1:def_3; ex T being DecoratedTree of F1() ex k being Element of NAT st ( y = k & f . y = T & T . {} = F2() & ( for t being Element of dom T holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } & ( for n being Element of NAT for x being set st x = T . t & P1[n,x] holds T . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66, A68; hence x is DecoratedTree of F1() by A69; ::_thesis: verum end; A70: for T1, T2 being DecoratedTree for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds T1 c= T2 proof let T1, T2 be DecoratedTree; ::_thesis: for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds T1 c= T2 let x, y be Element of NAT ; ::_thesis: ( T1 = f . x & T2 = f . y & x <= y implies T1 c= T2 ) assume that A71: T1 = f . x and A72: T2 = f . y and A73: x <= y ; ::_thesis: T1 c= T2 consider T19 being DecoratedTree of F1(), k1 being Element of NAT such that A74: ( x = k1 & f . x = T19 & T19 . {} = F2() & ( for t being Element of dom T19 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T19 . t] } & ( for n being Element of NAT for x being set st x = T19 . t & P1[n,x] holds T19 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66; consider T29 being DecoratedTree of F1(), k2 being Element of NAT such that A75: ( y = k2 & f . y = T29 & T29 . {} = F2() & ( for t being Element of dom T29 holds ( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T29 . t] } & ( for n being Element of NAT for x being set st x = T29 . t & P1[n,x] holds T29 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66; defpred S3[ Element of NAT ] means for t being Element of dom T1 st len t <= $1 holds ( t in dom T2 & T1 . t = T2 . t ); A76: S3[ 0 ] proof let t be Element of dom T1; ::_thesis: ( len t <= 0 implies ( t in dom T2 & T1 . t = T2 . t ) ) assume A77: len t <= 0 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) t = {} by A77; hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, TREES_1:22; ::_thesis: verum end; A78: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) assume A79: for t being Element of dom T1 st len t <= k holds ( t in dom T2 & T1 . t = T2 . t ) ; ::_thesis: S3[k + 1] let t be Element of dom T1; ::_thesis: ( len t <= k + 1 implies ( t in dom T2 & T1 . t = T2 . t ) ) assume len t <= k + 1 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) then A80: ( len t <= k or len t = k + 1 ) by NAT_1:8; now__::_thesis:_(_len_t_=_k_+_1_implies_(_t_in_dom_T2_&_T1_._t_=_T2_._t_)_) assume A81: len t = k + 1 ; ::_thesis: ( t in dom T2 & T1 . t = T2 . t ) reconsider p = t | (Seg k) as FinSequence of NAT by FINSEQ_1:18; p is_a_prefix_of t by TREES_1:def_1; then reconsider p = p as Element of dom T1 by TREES_1:20; A82: k <= k + 1 by NAT_1:11; A83: k + 1 <= k1 by A71, A74, A81; A84: len p = k by A81, A82, FINSEQ_1:17; A85: k < k1 by A83, NAT_1:13; A86: T1 . p = T2 . p by A79, A84; reconsider p9 = p as Element of dom T2 by A79, A84; t <> {} by A81; then consider q being FinSequence, x being set such that A87: t = q ^ <*x*> by FINSEQ_1:46; A88: ( p is_a_prefix_of t & q is_a_prefix_of t ) by A87, TREES_1:1, TREES_1:def_1; k + 1 = (len q) + 1 by A81, A87, FINSEQ_2:16; then A89: p = q by A84, A88, Th1, TREES_1:4; <*x*> is FinSequence of NAT by A87, FINSEQ_1:36; then A90: rng <*x*> c= NAT by FINSEQ_1:def_4; ( rng <*x*> = {x} & x in {x} ) by FINSEQ_1:38, TARSKI:def_1; then reconsider x = x as Element of NAT by A90; A91: p ^ <*x*> in succ p by A87, A89; succ p = { (p ^ <*i*>) where i is Element of NAT : P1[i,T1 . p] } by A71, A74, A84, A85; then consider i being Element of NAT such that A92: p ^ <*x*> = p ^ <*i*> and A93: P1[i,T1 . p] by A91; A94: k < k2 by A73, A74, A75, A85, XXREAL_0:2; then A95: succ p9 = { (p9 ^ <*l*>) where l is Element of NAT : P1[l,T2 . p9] } by A72, A75, A84; A96: x = i by A92, FINSEQ_2:17; A97: t in succ p9 by A86, A87, A89, A92, A93, A95; T19 . t = F3() . ((T19 . p),x) by A71, A74, A84, A85, A87, A89, A93, A96; hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, A84, A86, A87, A89, A93, A94, A96, A97; ::_thesis: verum end; hence ( t in dom T2 & T1 . t = T2 . t ) by A79, A80; ::_thesis: verum end; A98: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A76, A78); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in T2 ) assume A99: x in T1 ; ::_thesis: x in T2 then consider y, z being set such that A100: [y,z] = x by RELAT_1:def_1; A101: T1 . y = z by A99, A100, FUNCT_1:1; reconsider y = y as Element of dom T1 by A99, A100, FUNCT_1:1; len y <= len y ; then ( y in dom T2 & T1 . y = T2 . y ) by A98; hence x in T2 by A100, A101, FUNCT_1:1; ::_thesis: verum end; E is c=-linear proof let T1, T2 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not T1 in E or not T2 in E or T1,T2 are_c=-comparable ) assume A102: T1 in E ; ::_thesis: ( not T2 in E or T1,T2 are_c=-comparable ) then consider x being set such that A103: x in dom f and A104: T1 = f . x by FUNCT_1:def_3; assume A105: T2 in E ; ::_thesis: T1,T2 are_c=-comparable then consider y being set such that A106: y in dom f and A107: T2 = f . y by FUNCT_1:def_3; A108: T1 is DecoratedTree by A67, A102; A109: T2 is DecoratedTree by A67, A105; reconsider x = x, y = y as Element of NAT by A66, A103, A106; ( x <= y or y <= x ) ; hence ( T1 c= T2 or T2 c= T1 ) by A70, A104, A107, A108, A109; :: according to XBOOLE_0:def_9 ::_thesis: verum end; then reconsider T = union (rng f) as DecoratedTree of F1() by A67, Th36; take T ; ::_thesis: ( T . {} = F2() & ( for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) ) ) consider T9 being DecoratedTree of F1(), k being Element of NAT such that A110: ( 0 = k & f . 0 = T9 & T9 . {} = F2() & ( for t being Element of dom T9 holds ( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T9 . t] } & ( for n being Element of NAT for x being set st x = T9 . t & P1[n,x] holds T9 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66; {} in dom T9 by TREES_1:22; then A111: [{},F2()] in T9 by A110, FUNCT_1:1; T9 in rng f by A66, A110, FUNCT_1:def_3; then [{},F2()] in T by A111, TARSKI:def_4; hence T . {} = F2() by FUNCT_1:1; ::_thesis: for t being Element of dom T holds ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) A112: for T1 being DecoratedTree for x being set st T1 in E & x in dom T1 holds ( x in dom T & T1 . x = T . x ) proof let T1 be DecoratedTree; ::_thesis: for x being set st T1 in E & x in dom T1 holds ( x in dom T & T1 . x = T . x ) let x be set ; ::_thesis: ( T1 in E & x in dom T1 implies ( x in dom T & T1 . x = T . x ) ) assume that A113: T1 in E and A114: x in dom T1 ; ::_thesis: ( x in dom T & T1 . x = T . x ) [x,(T1 . x)] in T1 by A114, FUNCT_1:1; then [x,(T1 . x)] in T by A113, TARSKI:def_4; hence ( x in dom T & T1 . x = T . x ) by FUNCT_1:1; ::_thesis: verum end; let t be Element of dom T; ::_thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } & ( for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) thus succ t c= { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } :: according to XBOOLE_0:def_10 ::_thesis: ( { (t ^ <*k*>) where k is Element of NAT : P1[k,T . t] } c= succ t & ( for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } ) assume x in succ t ; ::_thesis: x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } then consider l being Element of NAT such that A115: x = t ^ <*l*> and A116: t ^ <*l*> in dom T ; [x,(T . x)] in T by A115, A116, FUNCT_1:1; then consider X being set such that A117: [x,(T . x)] in X and A118: X in rng f by TARSKI:def_4; consider y being set such that A119: y in NAT and A120: X = f . y by A66, A118, FUNCT_1:def_3; consider T1 being DecoratedTree of F1(), k1 being Element of NAT such that A121: ( y = k1 & f . y = T1 & T1 . {} = F2() & ( for t being Element of dom T1 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T1 . t] } & ( for n being Element of NAT for x being set st x = T1 . t & P1[n,x] holds T1 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66, A119; A122: t ^ <*l*> in dom T1 by A115, A117, A120, A121, FUNCT_1:1; then reconsider t9 = t, p = t ^ <*l*> as Element of dom T1 by TREES_1:21; len p <= k1 by A121; then (len t) + 1 <= k1 by FINSEQ_2:16; then A123: len t9 < k1 by NAT_1:13; then A124: succ t9 = { (t9 ^ <*i*>) where i is Element of NAT : P1[i,T1 . t9] } by A121; T1 . t = T . t by A112, A118, A120, A121, A123; hence x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } by A115, A122, A124; ::_thesis: verum end; [t,(T . t)] in T by FUNCT_1:1; then consider X being set such that A125: [t,(T . t)] in X and A126: X in E by TARSKI:def_4; consider y being set such that A127: y in NAT and A128: X = f . y by A66, A126, FUNCT_1:def_3; reconsider y = y as Element of NAT by A127; consider T1 being DecoratedTree of F1(), k1 being Element of NAT such that A129: ( y = k1 & f . y = T1 & T1 . {} = F2() & ( for t being Element of dom T1 holds ( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T1 . t] } & ( for n being Element of NAT for x being set st x = T1 . t & P1[n,x] holds T1 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66; consider T2 being DecoratedTree of F1(), k2 being Element of NAT such that A130: ( y + 1 = k2 & f . (y + 1) = T2 & T2 . {} = F2() & ( for t being Element of dom T2 holds ( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Element of NAT : P1[i,T2 . t] } & ( for n being Element of NAT for x being set st x = T2 . t & P1[n,x] holds T2 . (t ^ <*n*>) = F3() . (x,n) ) ) ) ) ) ) by A66; y <= y + 1 by NAT_1:11; then A131: T1 c= T2 by A70, A129, A130; reconsider t1 = t as Element of dom T1 by A125, A128, A129, FUNCT_1:1; A132: len t1 <= y by A129; A133: T2 . t = T . t by A125, A128, A129, A131, FUNCT_1:1; reconsider t2 = t as Element of dom T2 by A125, A128, A129, A131, FUNCT_1:1; A134: len t2 < y + 1 by A132, NAT_1:13; then A135: succ t2 = { (t2 ^ <*i*>) where i is Element of NAT : P1[i,T2 . t2] } by A130; thus { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } c= succ t ::_thesis: for n being Element of NAT st P1[n,T . t] holds T . (t ^ <*n*>) = F3() . ((T . t),n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } or x in succ t ) assume A136: x in { (t ^ <*i*>) where i is Element of NAT : P1[i,T . t] } ; ::_thesis: x in succ t then A137: ex l being Element of NAT st ( x = t ^ <*l*> & P1[l,T . t] ) ; A138: x in succ t2 by A130, A133, A134, A136; T2 in E by A66, A130, FUNCT_1:def_3; then x in dom T by A112, A138; hence x in succ t by A137; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( P1[n,T . t] implies T . (t ^ <*n*>) = F3() . ((T . t),n) ) assume A139: P1[n,T . t] ; ::_thesis: T . (t ^ <*n*>) = F3() . ((T . t),n) then A140: t ^ <*n*> in succ t2 by A133, A135; T2 in E by A66, A130, FUNCT_1:def_3; then T2 . (t ^ <*n*>) = T . (t ^ <*n*>) by A112, A140; hence T . (t ^ <*n*>) = F3() . ((T . t),n) by A130, A133, A134, A139; ::_thesis: verum end; theorem :: TREES_2:38 for T1, T2 being Tree st ( for n being Element of NAT holds T1 -level n = T2 -level n ) holds T1 = T2 proof let T1, T2 be Tree; ::_thesis: ( ( for n being Element of NAT holds T1 -level n = T2 -level n ) implies T1 = T2 ) assume A1: for n being Element of NAT holds T1 -level n = T2 -level n ; ::_thesis: T1 = T2 for p being FinSequence of NAT holds ( p in T1 iff p in T2 ) proof let p be FinSequence of NAT ; ::_thesis: ( p in T1 iff p in T2 ) A2: T1 = union { (T1 -level n) where n is Element of NAT : verum } by Th14; hereby ::_thesis: ( p in T2 implies p in T1 ) assume p in T1 ; ::_thesis: p in T2 then consider Y being set such that A3: p in Y and A4: Y in { (T1 -level n) where n is Element of NAT : verum } by A2, TARSKI:def_4; consider n being Element of NAT such that A5: Y = T1 -level n by A4; Y = T2 -level n by A1, A5; hence p in T2 by A3; ::_thesis: verum end; assume A6: p in T2 ; ::_thesis: p in T1 T2 = union { (T2 -level n) where n is Element of NAT : verum } by Th14; then consider Y being set such that A7: p in Y and A8: Y in { (T2 -level n) where n is Element of NAT : verum } by A6, TARSKI:def_4; consider n being Element of NAT such that A9: Y = T2 -level n by A8; Y = T1 -level n by A1, A9; hence p in T1 by A7; ::_thesis: verum end; hence T1 = T2 by Th5; ::_thesis: verum end; theorem :: TREES_2:39 for n being Element of NAT holds TrivialInfiniteTree -level n = {(n |-> 0)} proof set T = TrivialInfiniteTree ; let n be Element of NAT ; ::_thesis: TrivialInfiniteTree -level n = {(n |-> 0)} set L = { w where w is Element of TrivialInfiniteTree : len w = n } ; set f = n |-> 0; {(n |-> 0)} = { w where w is Element of TrivialInfiniteTree : len w = n } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { w where w is Element of TrivialInfiniteTree : len w = n } c= {(n |-> 0)} let a be set ; ::_thesis: ( a in {(n |-> 0)} implies a in { w where w is Element of TrivialInfiniteTree : len w = n } ) assume a in {(n |-> 0)} ; ::_thesis: a in { w where w is Element of TrivialInfiniteTree : len w = n } then A1: a = n |-> 0 by TARSKI:def_1; ( n |-> 0 in TrivialInfiniteTree & len (n |-> 0) = n ) by CARD_1:def_7; hence a in { w where w is Element of TrivialInfiniteTree : len w = n } by A1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { w where w is Element of TrivialInfiniteTree : len w = n } or a in {(n |-> 0)} ) assume a in { w where w is Element of TrivialInfiniteTree : len w = n } ; ::_thesis: a in {(n |-> 0)} then consider w being Element of TrivialInfiniteTree such that A2: ( a = w & len w = n ) ; w in TrivialInfiniteTree ; then ex k being Element of NAT st w = k |-> 0 ; then a = n |-> 0 by A2, CARD_1:def_7; hence a in {(n |-> 0)} by TARSKI:def_1; ::_thesis: verum end; hence TrivialInfiniteTree -level n = {(n |-> 0)} ; ::_thesis: verum end; theorem :: TREES_2:40 for X, Y being set for B being c=-linear Subset of (PFuncs (X,Y)) holds union B in PFuncs (X,Y) proof let X, Y be set ; ::_thesis: for B being c=-linear Subset of (PFuncs (X,Y)) holds union B in PFuncs (X,Y) let B be c=-linear Subset of (PFuncs (X,Y)); ::_thesis: union B in PFuncs (X,Y) for x being set st x in B holds x is Function ; then reconsider f = union B as Function by Th34; percases ( B <> {} or B = {} ) ; suppose B <> {} ; ::_thesis: union B in PFuncs (X,Y) then reconsider D = B as functional non empty set ; A1: now__::_thesis:_for_x_being_set_st_x_in__{__(dom_g)_where_g_is_Element_of_D_:_verum__}__holds_ x_c=_X let x be set ; ::_thesis: ( x in { (dom g) where g is Element of D : verum } implies x c= X ) assume x in { (dom g) where g is Element of D : verum } ; ::_thesis: x c= X then consider g being Element of D such that A2: x = dom g ; g in PFuncs (X,Y) by TARSKI:def_3; then ex f being Function st ( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def_3; hence x c= X by A2; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_set_st_x_in__{__(rng_g)_where_g_is_Element_of_D_:_verum__}__holds_ x_c=_Y let x be set ; ::_thesis: ( x in { (rng g) where g is Element of D : verum } implies x c= Y ) assume x in { (rng g) where g is Element of D : verum } ; ::_thesis: x c= Y then consider g being Element of D such that A4: x = rng g ; g in PFuncs (X,Y) by TARSKI:def_3; then ex f being Function st ( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def_3; hence x c= Y by A4; ::_thesis: verum end; rng f = union { (rng g) where g is Element of D : verum } by FUNCT_1:110; then A5: rng f c= Y by A3, ZFMISC_1:76; dom f = union { (dom g) where g is Element of D : verum } by FUNCT_1:110; then dom f c= X by A1, ZFMISC_1:76; hence union B in PFuncs (X,Y) by A5, PARTFUN1:def_3; ::_thesis: verum end; supposeA6: B = {} ; ::_thesis: union B in PFuncs (X,Y) {} is PartFunc of X,Y by RELSET_1:12; hence union B in PFuncs (X,Y) by A6, PARTFUN1:45, ZFMISC_1:2; ::_thesis: verum end; end; end;