hereby :: thesis: ( not W2 is_odd_substring_of W1, 0 implies ex b₁ being odd Element of NAT st b₁ = len W1 )

defpred S₁[ 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 ; :: thesis: 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
b₅ <= b₆ ) ) )
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 S₁[n]

proof

set j = (i -' 1) + (len W2);
set k = i -' 1;
take i -' 1 ; :: thesis: S₁[i -' 1]
A32: i -' 1 = i - 1 by A29, XREAL_1:233;
hence i -' 1 is even ; :: thesis: ( 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) ; :: thesis: for n being Nat st 1 <= n & n <= len W2 holds
W1 . ((i -' 1) + n) = W2 . n
let n be Nat; :: thesis: ( 1 <= n & n <= len W2 implies W1 . ((i -' 1) + n) = W2 . n )
assume A33: ( 1 <= n & n <= len W2 ) ; :: thesis: 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 ; :: thesis: verum

end;

consider k being Nat such that
A41: S₁[k] and
A42: for n being Nat st S₁[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; :: thesis: ( 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
b₄ <= b₅ ) ) )
k + (len W2) <= ((len W1) - (len W2)) + (len W2) by A41, XREAL_1:6;
hence j <= len W1 ; :: thesis: 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
b₄ <= b₅ ) )
take k = k; :: thesis: ( 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
b₃ <= b₄ ) )
thus j = k + (len W2) ; :: thesis: ( ( 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
b₃ <= b₄ ) )
thus for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n by A41; :: thesis: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
b₃ <= b₄
let l be even Nat; :: thesis: ( ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) implies b₂ <= b₃ )
assume A43: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ; :: thesis: b₂ <= b₃

per cases ( l <= (len W1) - (len W2) or l > (len W1) - (len W2) ) ;

suppose l <= (len W1) - (len W2) ; :: thesis: b₂ <= b₃

hence k <= l by A42, A43; :: thesis: verum

end;

suppose l > (len W1) - (len W2) ; :: thesis: b₂ <= b₃

hence k <= l by A41, XXREAL_0:2; :: thesis: verum

end;

end;

end;

assume not W2 is_odd_substring_of W1, 0 ; :: thesis: ex b₁ being odd Element of NAT st b₁ = len W1
thus ex b₁ being odd Element of NAT st b₁ = len W1 ; :: thesis: verum