let D be non empty set ; for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds
instr (1,(f ^ CR),CR) = (len f) + 1
let f, CR be FinSequence of D; ( not CR is_substring_of f,1 & CR separates_uniquely implies instr (1,(f ^ CR),CR) = (len f) + 1 )
assume that
A1:
not CR is_substring_of f,1
and
A2:
CR separates_uniquely
; instr (1,(f ^ CR),CR) = (len f) + 1
A3:
len CR > 0
by A1, FINSEQ_8:def 7;
then A4:
len CR >= 0 + 1
by NAT_1:13;
A5:
for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) holds
j >= (len f) + 1
proof
set i0 =
(len f) + 1;
set j0 =
(((len f) + 1) + (len CR)) -' 1;
let j be
Element of
NAT ;
( j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) implies j >= (len f) + 1 )
assume that A6:
j >= 1
and
j > 0
and A7:
CR is_preposition_of (f ^ CR) /^ (j -' 1)
;
j >= (len f) + 1
A8:
(
len CR > 0 implies ( 1
<= len ((f ^ CR) /^ (j -' 1)) &
mid (
((f ^ CR) /^ (j -' 1)),1,
(len CR))
= CR ) )
by A7, FINSEQ_8:def 8;
A9:
0 + j < (len CR) + j
by A3, XREAL_1:8;
then
j + 1
<= (len CR) + j
by NAT_1:13;
then A10:
j <= ((len CR) + j) - 1
by XREAL_1:19;
1
<= (len CR) + j
by A6, A9, XXREAL_0:2;
then A11:
((len CR) + j) - 1
>= 0
by XREAL_1:48;
then A12:
((len CR) + j) -' 1
= ((len CR) + j) - 1
by XREAL_0:def 2;
(len CR) - 1
>= 0
by A4, XREAL_1:48;
then ((((len CR) + j) -' 1) -' j) + 1 =
((((len CR) + j) - 1) - j) + 1
by A12, XREAL_0:def 2
.=
len CR
;
then A13:
((f ^ CR) /^ (j -' 1)) | (((((len CR) + j) -' 1) -' j) + 1) = CR
by A4, A8, FINSEQ_6:116;
(j + (len CR)) - 1
>= 0
by A6, NAT_1:12, XREAL_1:48;
then A14:
(j + (len CR)) -' 1
= (j + (len CR)) - 1
by XREAL_0:def 2;
A15:
(((len f) + 1) + (len CR)) -' 1 =
(((len f) + (len CR)) + 1) -' 1
.=
(len f) + (len CR)
by NAT_D:34
;
(((len f) + 1) + (len CR)) -' 1 =
(((len CR) + (len f)) + 1) -' 1
.=
(len CR) + (len f)
by NAT_D:34
;
then
mid (
(f ^ CR),
((len f) + 1),
((((len f) + 1) + (len CR)) -' 1))
= CR
by A4, Th5;
then A16:
smid (
(f ^ CR),
((len f) + 1),
((((len f) + 1) + (len CR)) -' 1))
= CR
by A4, A15, FINSEQ_8:4, XREAL_1:7;
A17:
(
len CR > 0 implies
len CR >= 0 + 1 )
by NAT_1:13;
then
j + (len CR) >= j + 1
by A1, FINSEQ_8:def 7, XREAL_1:7;
then A18:
(j + (len CR)) - 1
>= (j + 1) - 1
by XREAL_1:9;
j + (len CR) >= j + 1
by A1, A17, FINSEQ_8:def 7, XREAL_1:7;
then A19:
(j + (len CR)) - 1
>= (j + 1) - 1
by XREAL_1:9;
A20:
j - 1
>= 0
by A6, XREAL_1:48;
then A21:
j -' 1
= j - 1
by XREAL_0:def 2;
(j -' 1) + (len CR) =
(j - 1) + (len CR)
by A20, XREAL_0:def 2
.=
((len CR) + j) -' 1
by A11, XREAL_0:def 2
;
then A22:
mid (
(f ^ CR),
j,
((j -' 1) + (len CR)))
= CR
by A10, A12, A13, FINSEQ_6:def 3;
(j -' 1) + (len CR) =
(j - 1) + (len CR)
by A20, XREAL_0:def 2
.=
(j + (len CR)) - 1
;
then A23:
smid (
(f ^ CR),
j,
((j + (len CR)) -' 1))
= CR
by A14, A19, A22, FINSEQ_8:4;
now not j < (len f) + 1assume A24:
j < (len f) + 1
;
contradictionthen
((len f) + 1) - j > 0
by XREAL_1:50;
then A25:
((len f) + 1) -' j = ((len f) + 1) - j
by XREAL_0:def 2;
(((len f) + 1) + (len CR)) -' 1
<= len (f ^ CR)
by A15, FINSEQ_1:22;
then
((len f) + 1) -' j >= len CR
by A2, A6, A16, A23, A24, FINSEQ_8:def 6;
then
(((len f) + 1) - j) + j >= (len CR) + j
by A25, XREAL_1:7;
then
((len f) + 1) - 1
>= (j + (len CR)) - 1
by XREAL_1:9;
then
mid (
f,
j,
((j -' 1) + (len CR)))
= CR
by A6, A21, A18, A22, Th6;
then
j > len f
by A1, A6, FINSEQ_8:def 7;
hence
contradiction
by A24, NAT_1:13;
verum end;
hence
j >= (len f) + 1
;
verum
end;
(f ^ CR) /^ (len f) = CR
;
then
( (len f) + 1 <> 0 implies ( 1 <= (len f) + 1 & CR is_preposition_of (f ^ CR) /^ (((len f) + 1) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) holds
j >= (len f) + 1 ) ) )
by A5, NAT_1:11, NAT_D:34;
hence
instr (1,(f ^ CR),CR) = (len f) + 1
by FINSEQ_8:def 10; verum