let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
let f, g be FinSequence of D; :: thesis: for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
let n be Nat; :: thesis: ( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
assume A1: g is_substring_of f,n ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
per cases ( len g > 0 or len g = 0 ) ;
suppose A2: len g > 0 ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
then consider i being Nat such that
A3: ( n <= i & i <= len f ) and
A4: mid (f,i,((i -' 1) + (len g))) = g by A1, FINSEQ_8:def 7;
A5: 1 <= (n -' 1) + (len g) by A2, NAT_1:14;
A6: n <= (n -' 1) + (len g)
proof
A7: (n -' 1) + 1 <= (n -' 1) + (len g) by A2, NAT_1:14, XREAL_1:6;
per cases ( n -' 1 >= 1 or n -' 1 < 1 ) ;
suppose n -' 1 >= 1 ; :: thesis: n <= (n -' 1) + (len g)
hence n <= (n -' 1) + (len g) by A7, NAT_D:43; :: thesis: verum
end;
suppose n -' 1 < 1 ; :: thesis: n <= (n -' 1) + (len g)
then A8: n -' 1 = 0 by NAT_1:14;
then n <= 0 + 1 by NAT_D:36;
per cases then ( n = 0 or n = 1 ) by NAT_1:9;
suppose n = 0 ; :: thesis: n <= (n -' 1) + (len g)
hence n <= (n -' 1) + (len g) ; :: thesis: verum
end;
suppose n = 1 ; :: thesis: n <= (n -' 1) + (len g)
hence n <= (n -' 1) + (len g) by A7, A8; :: thesis: verum
end;
end;
end;
end;
end;
A9: (i -' 1) + (len g) <= len f by A3, A4, Th6;
n -' 1 <= i -' 1 by A3, NAT_D:42;
then (n -' 1) + (len g) <= (i -' 1) + (len g) by XREAL_1:6;
hence ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) ) by A5, A6, A9, XXREAL_0:2; :: thesis: verum
end;
suppose len g = 0 ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
hence ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) ) ; :: thesis: verum
end;
end;