let f be V26() standard special_circular_sequence; for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <= i2 holds
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
let g be FinSequence of (TOP-REAL 2); for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <= i2 holds
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
let i1, i2 be Nat; ( g is_a_part>_of f,i1,i2 & i1 <= i2 implies ( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) )
assume that
A1:
g is_a_part>_of f,i1,i2
and
A2:
i1 <= i2
; ( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
A3:
1 <= len g
by A1;
A4:
1 <= i1
by A1;
A5:
i1 + 1 <= len f
by A1;
then A6:
(i1 + 1) - 1 <= (len f) - 1
by XREAL_1:9;
then A7:
1 <= (len f) - 1
by A4, XXREAL_0:2;
then A8:
(len f) - 1 = (len f) -' 1
by NAT_D:39;
A16:
f . i2 = f . (S_Drop (((i1 + (len g)) -' 1),f))
by A1;
A17:
i2 + 1 <= len f
by A1;
i1 <= i1 + 1
by NAT_1:11;
then A21:
i1 <= len f
by A5, XXREAL_0:2;
A22:
0 <> (len f) -' 1
by A7, NAT_D:39;
A23:
len g < len f
by A1;
A24:
1 <= i2
by A1;
i2 <= i2 + 1
by NAT_1:11;
then A25:
i2 <= len f
by A17, XXREAL_0:2;
A26:
i2 <= (len f) -' 1
by A17, NAT_D:49;
then
1 <= (len f) -' 1
by A24, XXREAL_0:2;
then
(len f) -' 1 < len f
by NAT_D:51;
then A27:
i2 < len f
by A26, XXREAL_0:2;
now ( ( i2 < S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 > S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 = S_Drop (((i1 + (len g)) -' 1),f) & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) )per cases
( i2 < S_Drop (((i1 + (len g)) -' 1),f) or i2 > S_Drop (((i1 + (len g)) -' 1),f) or i2 = S_Drop (((i1 + (len g)) -' 1),f) )
by XXREAL_0:1;
case A28:
i2 < S_Drop (
((i1 + (len g)) -' 1),
f)
;
contradiction
i2 <= len f
by A17, NAT_D:46;
then A29:
f /. i2 = f . i2
by A24, FINSEQ_4:15;
A30:
1
<= S_Drop (
((i1 + (len g)) -' 1),
f)
by A24, A28, XXREAL_0:2;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f))
by A24, A9, A28, GOBOARD7:36;
hence
contradiction
by A16, A9, A29, A30, FINSEQ_4:15;
verum end; case A31:
i2 > S_Drop (
((i1 + (len g)) -' 1),
f)
;
contradiction
i2 <= len f
by A17, NAT_D:46;
then A32:
f /. i2 = f . i2
by A24, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f))
by A18, A27, A31, GOBOARD7:36;
hence
contradiction
by A16, A18, A9, A32, FINSEQ_4:15;
verum end; case A33:
i2 = S_Drop (
((i1 + (len g)) -' 1),
f)
;
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )now ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) )per cases
( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 )
;
case A34:
((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0
;
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
ex
n being
Nat st
(
(i1 + (len g)) -' 1
= (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) &
((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 )
by A22, NAT_D:def 2;
then consider n being
Nat such that A35:
(i1 + (len g)) -' 1
= (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1))
;
A36:
(i1 + (len g)) -' 1
= (((len f) -' 1) * n) + i2
by A33, A34, A35, Def1;
now ( ( n = 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) or ( n <> 0 & contradiction ) )per cases
( n = 0 or n <> 0 )
;
case A37:
n = 0
;
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )A38:
dom g = Seg (len g)
by FINSEQ_1:def 3;
A39:
(i1 + (len g)) -' 1
= (i1 + (len g)) - 1
by A4, NAT_1:12, XREAL_1:233;
A40:
i2 = (i1 + (len g)) -' 1
by A33, A34, A35, A37, Def1;
then A41:
(i2 + 1) - i1 = len g
by A39;
A42:
for
j being
Nat st
j in dom g holds
g . j = (mid (f,i1,i2)) . j
proof
let j be
Nat;
( j in dom g implies g . j = (mid (f,i1,i2)) . j )
assume A43:
j in dom g
;
g . j = (mid (f,i1,i2)) . j
then A44:
1
<= j
by A38, FINSEQ_1:1;
then A45:
(i1 + j) -' 1
= (i1 + j) - 1
by NAT_D:37;
i1 + j >= 1
+ 1
by A4, A44, XREAL_1:7;
then A46:
(i1 + j) -' 1
<> 0
by A45;
A47:
j <= len g
by A38, A43, FINSEQ_1:1;
then
j + i1 <= ((i2 - i1) + 1) + i1
by A40, A39, XREAL_1:6;
then A48:
i1 + j <= len f
by A17, XXREAL_0:2;
g . j = f . (S_Drop (((i1 + j) -' 1),f))
by A1, A44, A47;
hence
g . j = (mid (f,i1,i2)) . j
by A2, A4, A25, A41, A44, A47, A49, FINSEQ_6:122;
verum
end; A51:
(i2 - i1) + 1
= len g
by A40, A39;
then
len g = (i2 -' i1) + 1
by A2, XREAL_1:233;
then
len (mid (f,i1,i2)) = len g
by A2, A4, A24, A21, A25, FINSEQ_6:118;
hence
(
len g = (i2 -' i1) + 1 &
g = mid (
f,
i1,
i2) )
by A2, A51, A42, FINSEQ_2:9, XREAL_1:233;
verum end; end; end; hence
(
len g = (i2 -' i1) + 1 &
g = mid (
f,
i1,
i2) )
;
verum end; case A54:
((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0
;
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
ex
n being
Nat st
(
(i1 + (len g)) -' 1
= (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) &
((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 )
by A22, NAT_D:def 2;
then consider n being
Nat such that A55:
(i1 + (len g)) -' 1
= (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1))
;
then
n >= 0 + 1
by NAT_1:13;
then A59:
n = 1
by A56, XXREAL_0:1;
(i1 + (len g)) -' 1
= i2 * n
by A33, A54, A55, Def1;
then A60:
(i1 + (len g)) - 1
= i2
by A24, A59, NAT_D:39;
A61:
i2 - i1 = i2 -' i1
by A2, XREAL_1:233;
then A62:
len g = (i2 -' i1) + 1
by A60;
A63:
dom g = Seg (len g)
by FINSEQ_1:def 3;
A64:
for
j being
Nat st
j in dom g holds
g . j = (mid (f,i1,i2)) . j
proof
let j be
Nat;
( j in dom g implies g . j = (mid (f,i1,i2)) . j )
assume A65:
j in dom g
;
g . j = (mid (f,i1,i2)) . j
then A66:
1
<= j
by A63, FINSEQ_1:1;
then A67:
(i1 + j) -' 1
= (i1 + j) - 1
by NAT_D:37;
A68:
j <= len g
by A63, A65, FINSEQ_1:1;
then
j + i1 <= ((i2 - i1) + 1) + i1
by A60, XREAL_1:6;
then A69:
i1 + j <= len f
by A17, XXREAL_0:2;
i1 + j >= 1
+ 1
by A4, A66, XREAL_1:7;
then A70:
(i1 + j) -' 1
<> 0
by A67;
g . j = f . (S_Drop (((i1 + j) -' 1),f))
by A1, A66, A68;
hence
g . j = (mid (f,i1,i2)) . j
by A2, A4, A25, A62, A66, A68, A71, FINSEQ_6:122;
verum
end;
len (mid (f,i1,i2)) = len g
by A2, A4, A24, A21, A25, A62, FINSEQ_6:118;
hence
(
len g = (i2 -' i1) + 1 &
g = mid (
f,
i1,
i2) )
by A60, A61, A64, FINSEQ_2:9;
verum end; end; end; hence
(
len g = (i2 -' i1) + 1 &
g = mid (
f,
i1,
i2) )
;
verum end; end; end;
hence
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )
; verum