let f be V26() standard special_circular_sequence; for i1, i2 being Nat st 1 <= i2 & i1 > i2 & i1 < len f holds
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
let i1, i2 be Nat; ( 1 <= i2 & i1 > i2 & i1 < len f implies (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2 )
assume that
A1:
1 <= i2
and
A2:
i1 > i2
and
A3:
i1 < len f
; (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
A4: len (mid (f,1,i2)) =
len (f | i2)
by A1, FINSEQ_6:116
.=
i2
by A2, A3, FINSEQ_1:59, XXREAL_0:2
;
A5:
1 <= i1
by A1, A2, XXREAL_0:2;
len f < (len f) + 1
by NAT_1:13;
then
(len f) - 1 < ((len f) + 1) - 1
by XREAL_1:9;
then A6:
(len f) -' 1 < len f
by A3, A5, XREAL_1:233, XXREAL_0:2;
A7:
i1 + 1 <= len f
by A3, NAT_1:13;
then
(i1 + 1) - 1 <= (len f) - 1
by XREAL_1:9;
then A8:
i1 <= (len f) -' 1
by A3, A5, XREAL_1:233, XXREAL_0:2;
then A9:
1 <= (len f) -' 1
by A5, XXREAL_0:2;
then len (mid (f,i1,((len f) -' 1))) =
(((len f) -' 1) -' i1) + 1
by A3, A5, A8, A6, FINSEQ_6:118
.=
(((len f) -' 1) - i1) + 1
by A8, XREAL_1:233
.=
(((len f) - 1) - i1) + 1
by A3, A5, XREAL_1:233, XXREAL_0:2
.=
(len f) - i1
;
then A10: len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) =
((len f) - i1) + i2
by A4, FINSEQ_1:22
.=
(len f) - (i1 - i2)
;
A11:
i2 < len f
by A2, A3, XXREAL_0:2;
then A12:
i2 + 1 <= len f
by NAT_1:13;
then
(i2 + 1) - 1 <= (len f) - 1
by XREAL_1:9;
then A13:
i2 <= (len f) -' 1
by A3, A5, XREAL_1:233, XXREAL_0:2;
A14:
for i being Nat st 1 <= i & i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) holds
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
proof
let i be
Nat;
( 1 <= i & i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) )
assume that A15:
1
<= i
and A16:
i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)))
;
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
A17:
(i1 + i) -' 1
= (i1 + i) - 1
by A15, NAT_D:37;
A18:
(len f) - i1 = (len f) -' i1
by A3, XREAL_1:233;
A19:
(((len f) -' 1) -' i1) + 1 =
(((len f) -' 1) - i1) + 1
by A8, XREAL_1:233
.=
(((len f) - 1) - i1) + 1
by A3, A5, XREAL_1:233, XXREAL_0:2
.=
(len f) - i1
;
A20:
len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1
by A3, A5, A8, A9, A6, FINSEQ_6:118;
now ( ( i <= len (mid (f,i1,((len f) -' 1))) & ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) ) or ( i > len (mid (f,i1,((len f) -' 1))) & ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) ) )per cases
( i <= len (mid (f,i1,((len f) -' 1))) or i > len (mid (f,i1,((len f) -' 1))) )
;
case A21:
i <= len (mid (f,i1,((len f) -' 1)))
;
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))then
i1 + i <= i1 + ((((len f) -' 1) -' i1) + 1)
by A20, XREAL_1:6;
then
i1 + i <= ((((len f) -' 1) - i1) + 1) + i1
by A8, XREAL_1:233;
then
i1 + i <= ((len f) -' 1) + 1
;
then
i1 + i <= len f
by A3, A5, XREAL_1:235, XXREAL_0:2;
then
(i1 + i) -' 1
<= (len f) - 1
by A17, XREAL_1:9;
then A22:
(i1 + i) -' 1
<= (len f) -' 1
by A3, A5, XREAL_1:233, XXREAL_0:2;
0 <= i - 1
by A15, XREAL_1:48;
then A23:
1
+ 0 <= i1 + (i - 1)
by A5, XREAL_1:7;
i in dom (mid (f,i1,((len f) -' 1)))
by A15, A21, FINSEQ_3:25;
then A24:
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = (mid (f,i1,((len f) -' 1))) . i
by FINSEQ_1:def 7;
(mid (f,i1,((len f) -' 1))) . i = f . ((i1 + i) -' 1)
by A3, A5, A8, A9, A6, A15, A21, FINSEQ_6:118;
hence
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
by A17, A24, A23, A22, Th22;
verum end; case A25:
i > len (mid (f,i1,((len f) -' 1)))
;
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))then
i >= ((len f) -' i1) + 1
by A20, A19, A18, NAT_1:13;
then A26:
i - ((len f) -' i1) >= (((len f) -' i1) + 1) - ((len f) -' i1)
by XREAL_1:9;
then A27:
1
<= i -' ((len f) -' i1)
by NAT_D:39;
A28:
(len f) - i1 = (len f) -' i1
by A3, XREAL_1:233;
i - ((len f) - i1) <= (((len f) - i1) + i2) - ((len f) - i1)
by A10, A16, XREAL_1:9;
then A29:
i -' ((len f) -' i1) <= i2
by A28, A26, NAT_D:39;
then A30:
i -' ((len f) -' i1) <= (len f) -' 1
by A13, XXREAL_0:2;
((len f) -' 1) + (i -' ((len f) -' i1)) =
((len f) -' 1) + (i - ((len f) -' i1))
by A20, A19, A18, A25, XREAL_1:233
.=
(((len f) -' 1) + i) - ((len f) -' i1)
.=
(((len f) - 1) + i) - ((len f) -' i1)
by A3, A5, XREAL_1:233, XXREAL_0:2
.=
(((len f) - 1) + i) - ((len f) - i1)
by A3, XREAL_1:233
.=
(i + i1) - 1
.=
(i1 + i) -' 1
by A15, NAT_D:37
;
then A31:
S_Drop (
((i1 + i) -' 1),
f) =
S_Drop (
(i -' ((len f) -' i1)),
f)
by Th23
.=
i -' ((len f) -' i1)
by A27, A30, Th22
;
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i =
(mid (f,1,i2)) . (i - (len (mid (f,i1,((len f) -' 1)))))
by A16, A25, FINSEQ_6:108
.=
(mid (f,1,i2)) . (i -' ((len f) -' i1))
by A20, A19, A18, A25, XREAL_1:233
.=
f . (i -' ((len f) -' i1))
by A11, A27, A29, FINSEQ_6:123
;
hence
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
by A31;
verum end;
hence
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
;
verum
end;
i1 - i2 > 0
by A2, XREAL_1:50;
then
len f < (len f) + (i1 - i2)
by XREAL_1:29;
then A32:
(len f) - (i1 - i2) < ((len f) + (i1 - i2)) - (i1 - i2)
by XREAL_1:9;
A33:
len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) = (len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2)))
by FINSEQ_1:22;
then
len (mid (f,1,i2)) <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)))
by NAT_1:11;
then A34:
1 <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)))
by A1, A4, XXREAL_0:2;
len (mid (f,i1,((len f) -' 1))) < (len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2)))
by A1, A4, XREAL_1:29;
then ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . (len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)))) =
(mid (f,1,i2)) . (((len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2)))) - (len (mid (f,i1,((len f) -' 1)))))
by A33, FINSEQ_6:108
.=
f . i2
by A1, A11, Th10
;
hence
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
by A1, A5, A12, A7, A34, A10, A32, A14; verum