let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n being Element of NAT st not g is_substring_of f,n holds
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
let f, g be FinSequence of D; :: thesis: for n being Element of NAT st not g is_substring_of f,n holds
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
let n be Element of NAT ; :: thesis: ( not g is_substring_of f,n implies for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g )
assume A1: not g is_substring_of f,n ; :: thesis: for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
now
let i be Element of NAT ; :: thesis: ( n <= i & 0 < i implies mid (f,i,((i -' 1) + (len g))) <> g )
assume that
A2: n <= i and
A3: 0 < i ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g
now
per cases ( i <= len f or i > len f ) ;
case i <= len f ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g
hence mid (f,i,((i -' 1) + (len g))) <> g by A1, A2, Def7; :: thesis: verum
end;
case A4: i > len f ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g
now
per cases ( i <= (i -' 1) + (len g) or i > (i -' 1) + (len g) ) ;
case A5: i <= (i -' 1) + (len g) ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g
then A6: mid (f,i,((i -' 1) + (len g))) = (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by FINSEQ_6:def 3;
A7: now
per cases ( i -' 1 <= len f or i -' 1 > len f ) ;
case A8: i -' 1 <= len f ; :: thesis: len (f /^ (i -' 1)) = 0
i >= (len f) + 1 by A4, NAT_1:13;
then A9: i - 1 >= ((len f) + 1) - 1 by XREAL_1:9;
0 + 1 <= i by A3, NAT_1:13;
then 0 <= i - 1 by XREAL_1:48;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A10: i -' 1 = len f by A8, A9, XXREAL_0:1;
len (f /^ (i -' 1)) = (len f) - (i -' 1) by A8, RFINSEQ:def 1;
hence len (f /^ (i -' 1)) = 0 by A10; :: thesis: verum
end;
case i -' 1 > len f ; :: thesis: len (f /^ (i -' 1)) = 0
then f /^ (i -' 1) = <*> D by RFINSEQ:def 1;
hence len (f /^ (i -' 1)) = 0 ; :: thesis: verum
end;
end;
end;
then f /^ (i -' 1) = <*> D ;
then A11: (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = <*> D by A7, FINSEQ_1:58;
now
assume A12: mid (f,i,((i -' 1) + (len g))) = g ; :: thesis: contradiction
0 + 1 <= i by A3, NAT_1:13;
then A13: 0 <= i - 1 by XREAL_1:48;
i < i + 1 by XREAL_1:29;
then i - 1 < (i + 1) - 1 by XREAL_1:9;
hence contradiction by A5, A6, A7, A11, A12, A13, XREAL_0:def 2; :: thesis: verum
end;
hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum
end;
case A14: i > (i -' 1) + (len g) ; :: thesis: contradiction
now
assume len g > 0 ; :: thesis: contradiction
then len g >= 0 + 1 by NAT_1:13;
then A15: (i -' 1) + (len g) >= (i -' 1) + 1 by XREAL_1:7;
0 + 1 <= i by A3, NAT_1:13;
then 0 <= i - 1 by XREAL_1:48;
then i -' 1 = i - 1 by XREAL_0:def 2;
hence contradiction by A14, A15; :: thesis: verum
end;
hence contradiction by A1, Def7; :: thesis: verum
end;
end;
end;
hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum
end;
end;
end;
hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum
end;
hence for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum