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 ]
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;
A8:
k < card C
by A6, A7, 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:19;
A11:
len q = k
by A10, FINSEQ_1:21;
A12:
card (ProperPrefixes q) = k
by A11, TREES_1:68;
A13:
card (ProperPrefixes q) in card C
by A8, A12, NAT_1:45;
A14:
C \ (ProperPrefixes q) <> {}
by A13, CARD_2:4;
consider x being
Element of
C \ (ProperPrefixes q);
A15:
x in C
by A14, XBOOLE_0:def 5;
A16:
not
x in ProperPrefixes q
by A14, XBOOLE_0:def 5;
reconsider x =
x as
Element of
W by A15;
A17:
card ((ProperPrefixes q) \/ {x}) = k + 1
by A12, A16, CARD_2:54;
A18:
card ((ProperPrefixes q) \/ {x}) in card C
by A6, A17, NAT_1:45;
A19:
C \ ((ProperPrefixes q) \/ {x}) <> {}
by A18, CARD_2:4;
consider y being
Element of
C \ ((ProperPrefixes q) \/ {x});
A20:
y in C
by A19, XBOOLE_0:def 5;
A21:
not
y in (ProperPrefixes q) \/ {x}
by A19, XBOOLE_0:def 5;
reconsider y =
y as
Element of
W by A20;
A22:
not
y in ProperPrefixes q
by A21, XBOOLE_0:def 3;
A23:
not
y in {x}
by A21, XBOOLE_0:def 3;
A24:
q is_a_prefix_of p
by TREES_1:def 1;
A25:
q is_a_prefix_of x
by A9, A15, A16, A24, Th24;
A26:
q is_a_prefix_of y
by A9, A20, A22, A24, Th24;
A27:
x <> y
by A23, TARSKI:def 1;
A28:
(
x = q or
x <> q )
;
A29:
(
q is_a_proper_prefix_of y or
q is_a_proper_prefix_of x )
by A25, A26, A27, A28, XBOOLE_0:def 8;
A30:
(
k < len x or
k < len y )
by A11, A29, TREES_1:24;
A31:
(
k + 1
<= len x or
k + 1
<= len y )
by A30, NAT_1:13;
thus
ex
p being
FinSequence of
NAT st
(
p in C &
len p >= k + 1 )
by A15, A20, A31;
:: thesis: verum
end;
A32:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A1, A4);
thus
( card C > n implies ex p being FinSequence of NAT st
( p in C & len p >= n ) )
by A32; :: thesis: verum