hereby ( not W2 is_odd_substring_of W1, 0 implies ex b1 being odd Element of NAT st b1 = len W1 )
defpred S1[
Nat]
means ( $1 is
even & $1
<= (len W1) - (len W2) & ( for
n being
Nat st 1
<= n &
n <= len W2 holds
W1 . ($1 + n) = W2 . n ) );
assume
W2 is_odd_substring_of W1,
0
;
ex j being odd Element of NAT st
( j <= len W1 & ex k being even Nat st
( j = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b5 <= b6 ) ) )then
W2 is_odd_substring_of W1,1
by Th18;
then consider i being
odd Nat such that A29:
( 1
<= i &
i <= len W1 )
and A30:
mid (
W1,
i,
((i -' 1) + (len W2)))
= W2
;
A31:
ex
n being
Nat st
S1[
n]
proof
set j =
(i -' 1) + (len W2);
set k =
i -' 1;
take
i -' 1
;
S1[i -' 1]
A32:
i -' 1
= i - 1
by A29, XREAL_1:233;
hence
i -' 1 is
even
;
( i -' 1 <= (len W1) - (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . ((i -' 1) + n) = W2 . n ) )
(i -' 1) + (len W2) <= len W1
by A29, A30, Th6;
then
((i -' 1) + (len W2)) - (len W2) <= (len W1) - (len W2)
by XREAL_1:9;
hence
i -' 1
<= (len W1) - (len W2)
;
for n being Nat st 1 <= n & n <= len W2 holds
W1 . ((i -' 1) + n) = W2 . n
let n be
Nat;
( 1 <= n & n <= len W2 implies W1 . ((i -' 1) + n) = W2 . n )
assume A33:
( 1
<= n &
n <= len W2 )
;
W1 . ((i -' 1) + n) = W2 . n
then A34:
( 1
<= n &
n <= len (mid (W1,i,((i -' 1) + (len W2)))) )
by A30;
len W2 >= 1
by FINSEQ_1:20;
then A36:
1
- 1
<= (len W2) - 1
by XREAL_1:9;
(i -' 1) + (len W2) =
(i + (len W2)) -' 1
by A29, NAT_D:38
.=
(i + (len W2)) - 1
by A29, NAT_D:37
;
then A38:
(i + ((len W2) - 1)) - ((len W2) - 1) <= ((i -' 1) + (len W2)) - 0
by A36, XREAL_1:13;
A39:
1
<= (i -' 1) + (len W2)
by A29, A38, XXREAL_0:2;
A40:
( 1
<= (i -' 1) + (len W2) &
(i -' 1) + (len W2) <= len W1 )
by A39, A29, A30, Th6;
thus W1 . ((i -' 1) + n) =
W1 . ((n + i) - 1)
by A32
.=
W1 . ((n + i) -' 1)
by A33, NAT_D:37
.=
W2 . n
by A29, A30, A34, A38, A40, FINSEQ_6:118
;
verum
end; consider k being
Nat such that A41:
S1[
k]
and A42:
for
n being
Nat st
S1[
n] holds
k <= n
from NAT_1:sch 5(A31);
reconsider k =
k as
even Nat by A41;
reconsider j =
k + (len W2) as
odd Element of
NAT ;
take j =
j;
( j <= len W1 & ex k being even Nat st
( j = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b4 <= b5 ) ) )
k + (len W2) <= ((len W1) - (len W2)) + (len W2)
by A41, XREAL_1:6;
hence
j <= len W1
;
ex k being even Nat st
( j = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b4 <= b5 ) )take k =
k;
( j = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b3 <= b4 ) )thus
j = k + (len W2)
;
( ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b3 <= b4 ) )thus
for
n being
Nat st 1
<= n &
n <= len W2 holds
W1 . (k + n) = W2 . n
by A41;
for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b3 <= b4let l be
even Nat;
( ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) implies b2 <= b3 )assume A43:
for
n being
Nat st 1
<= n &
n <= len W2 holds
W1 . (l + n) = W2 . n
;
b2 <= b3
end;
assume
not W2 is_odd_substring_of W1, 0
; ex b1 being odd Element of NAT st b1 = len W1
thus
ex b1 being odd Element of NAT st b1 = len W1
; verum