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 & ( 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 + 1 & ( 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
A2: ( 1 <= i & i <= len W1 ) and
A3: mid (W1,i,((i -' 1) + (len W2))) = W2 ;
A4: ex n being Nat st S₁[n]

proof

set j = (i -' 1) + (len W2);
reconsider k = i - 1 as Nat by CHORD:2;
take k ; :: thesis: S₁[k]
thus k is even ; :: thesis: ( k <= len W1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) )
i - 1 <= (len W1) - 0 by A2, XREAL_1:13;
hence k <= len W1 ; :: thesis: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n
let n be Nat; :: thesis: ( 1 <= n & n <= len W2 implies W1 . (k + n) = W2 . n )
assume A5: ( 1 <= n & n <= len W2 ) ; :: thesis: W1 . (k + n) = W2 . n
then A6: ( 1 <= n & n <= len (mid (W1,i,((i -' 1) + (len W2)))) ) by A3;
1 - 1 <= (len W2) - 1 by FINSEQ_1:20, XREAL_1:9;
then A8: 0 <= (len W2) - 1 ;
(i -' 1) + (len W2) = (i + (len W2)) -' 1 by A2, NAT_D:38
.= (i + (len W2)) - 1 by A2, NAT_D:37 ;
then A10: (i + ((len W2) - 1)) - ((len W2) - 1) <= ((i -' 1) + (len W2)) - 0 by A8, XREAL_1:13;
then A11: 1 <= (i -' 1) + (len W2) by A2, XXREAL_0:2;
A12: ( 1 <= (i -' 1) + (len W2) & (i -' 1) + (len W2) <= len W1 ) by A11, A2, A3, Th6;
thus W1 . (k + n) = W1 . ((n + i) - 1)
.= W1 . ((n + i) -' 1) by A5, NAT_D:37
.= W2 . n by A2, A3, A6, A10, A12, FINSEQ_6:118 ; :: thesis: verum

end;

consider k being Nat such that
A13: S₁[k] and
A14: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A4);
reconsider k = k as even Nat by A13;
reconsider j = k + 1 as odd Element of NAT ;
take j = j; :: thesis: ( j <= len W1 & ex k being even Nat st
( j = k + 1 & ( 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 <= len W1 by A13, Th1; :: thesis: ex k being even Nat st
( j = k + 1 & ( 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 + 1 & ( 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 + 1 ; :: 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 A13; :: 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 A15: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ; :: thesis: b₂ <= b₃

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

suppose l <= len W1 ; :: thesis: b₂ <= b₃

hence k <= l by A14, A15; :: thesis: verum

end;

suppose l > len W1 ; :: thesis: b₂ <= b₃

hence k <= l by A13, 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