let T be Tree; :: thesis: ( ( for n being 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 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 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 Nat st
( x ^ <*n*> in T & S1[x ^ <*n*>] )
proof
let x be Element of T; :: thesis: ( S1[x] implies ex n being Nat st
( x ^ <*n*> in T & S1[x ^ <*n*>] ) )
assume that
A4: S1[x] and
A5: for n being Nat st x ^ <*n*> in T holds
not S1[x ^ <*n*>] ; :: thesis: contradiction
A6: succ x is finite by A2;
defpred S2[ object , 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 object st y in succ x holds
ex n being Nat st S2[y,n]
proof
let y be object ; :: thesis: ( y in succ x implies ex n being Nat st S2[y,n] )
assume y in succ x ; :: thesis: ex n being Nat st S2[y,n]
then consider k being Nat such that
A8: y = x ^ <*k*> and
A9: x ^ <*k*> in T ;
consider n being 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 object st y in succ x holds
ex n being Nat st
( f . y = n & S2[y,n] & ( for m being Nat st S2[y,m] holds
n <= m ) ) from TREES_2:sch 4(A7);
 consider k being Nat such that
A13: for m being 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 ;
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 Nat ;
A25: x ^ <*l*> in succ x by A21, A22, A23;
then consider n being 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 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 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[ object ] means ex t being Element of T st
( t = $1 & S1[t] );
defpred S3[ object , object ] means ex p being FinSequence of NAT ex n being Nat st
( $1 = p & p ^ <*n*> in T & $2 = p ^ <*n*> );
A33: ( e in T & S2[e] ) by A28;
A34: for x being object st x in T & S2[x] holds
ex y being object st
( y in T & S3[x,y] & S2[y] )
proof
let x be object ; :: thesis: ( x in T & S2[x] implies ex y being object st
( y in T & S3[x,y] & S2[y] ) )
assume x in T ; :: thesis: ( not S2[x] or ex y being object 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 object st
( y in T & S3[x,y] & S2[y] )
consider n being 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 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 Nat holds
( ex p being FinSequence of NAT ex n being 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 Nat ;
consider r being FinSequence of NAT , l being 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; :: 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 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 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 object such that
A55: x in NAT and
A56: p = f . x by A39, A53, FUNCT_1:def 3;
consider y being object such that
A57: y in NAT and
A58: q = f . y by A39, A54, FUNCT_1:def 3;
reconsider x = x, y = y as 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[ 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 Nat st S4[k] holds
S4[k + 1]
proof
let k be 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 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 Nat holds S4[k] from NAT_1:sch 2(A59, A60);
 f is one-to-one
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: 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 Nat by A39;
consider p being FinSequence of NAT , n being 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 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