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