let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of 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 Element of NAT ; :: thesis: ( 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 A1:
( 1 <= i2 & i1 > i2 & i1 < len f )
; :: thesis: (mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,i1,i2
then A2:
1 <= i1
by XXREAL_0:2;
A3:
i2 < len f
by A1, XXREAL_0:2;
then A4:
i2 + 1 <= len f
by NAT_1:13;
A5:
i1 + 1 <= len f
by A1, NAT_1:13;
then
(i1 + 1) - 1 <= (len f) - 1
by XREAL_1:11;
then A6:
i1 <= (len f) -' 1
by A1, A2, XREAL_1:235, XXREAL_0:2;
then A7:
1 <= (len f) -' 1
by A2, XXREAL_0:2;
(i2 + 1) - 1 <= (len f) - 1
by A4, XREAL_1:11;
then A8:
i2 <= (len f) -' 1
by A1, A2, XREAL_1:235, XXREAL_0:2;
len f < (len f) + 1
by NAT_1:13;
then
(len f) - 1 < ((len f) + 1) - 1
by XREAL_1:11;
then A9:
(len f) -' 1 < len f
by A1, A2, XREAL_1:235, XXREAL_0:2;
A10:
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:35;
A11: len (mid f,1,i2) =
len (f | i2)
by A1, JORDAN3:25
.=
i2
by A1, FINSEQ_1:80, XXREAL_0:2
;
then
len (mid f,i1,((len f) -' 1)) < (len (mid f,i1,((len f) -' 1))) + (len (mid f,1,i2))
by A1, XREAL_1:31;
then A12: ((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 A10, JORDAN3:15
.=
f . i2
by A1, A3, Th22
;
len (mid f,1,i2) <= len ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2))
by A10, NAT_1:11;
then A13:
1 <= len ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2))
by A1, A11, XXREAL_0:2;
len (mid f,i1,((len f) -' 1)) =
(((len f) -' 1) -' i1) + 1
by A1, A2, A6, A7, A9, JORDAN3:27
.=
(((len f) -' 1) - i1) + 1
by A6, XREAL_1:235
.=
(((len f) - 1) - i1) + 1
by A1, A2, XREAL_1:235, XXREAL_0:2
.=
(len f) - i1
;
then A14: len ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) =
((len f) - i1) + i2
by A11, FINSEQ_1:35
.=
(len f) - (i1 - i2)
;
i1 - i2 > 0
by A1, XREAL_1:52;
then
len f < (len f) + (i1 - i2)
by XREAL_1:31;
then A15:
(len f) - (i1 - i2) < ((len f) + (i1 - i2)) - (i1 - i2)
by XREAL_1:11;
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;
:: thesis: ( 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 A16:
( 1
<= i &
i <= len ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) )
;
:: thesis: ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)
A17:
len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1
by A1, A2, A6, A7, A9, JORDAN3:27;
A18:
(((len f) -' 1) -' i1) + 1 =
(((len f) -' 1) - i1) + 1
by A6, XREAL_1:235
.=
(((len f) - 1) - i1) + 1
by A1, A2, XREAL_1:235, XXREAL_0:2
.=
(len f) - i1
;
A19:
(len f) - i1 = (len f) -' i1
by A1, XREAL_1:235;
A20:
(i1 + i) -' 1
= (i1 + i) - 1
by A16, NAT_D:37;
A21:
i in NAT
by ORDINAL1:def 13;
now per cases
( i <= len (mid f,i1,((len f) -' 1)) or i > len (mid f,i1,((len f) -' 1)) )
;
case A22:
i <= len (mid f,i1,((len f) -' 1))
;
:: thesis: ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)then
i in dom (mid f,i1,((len f) -' 1))
by A16, FINSEQ_3:27;
then A23:
((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = (mid f,i1,((len f) -' 1)) . i
by FINSEQ_1:def 7;
A24:
(mid f,i1,((len f) -' 1)) . i = f . ((i1 + i) -' 1)
by A1, A2, A6, A7, A9, A16, A21, A22, JORDAN3:27;
0 <= i - 1
by A16, XREAL_1:50;
then A25:
1
+ 0 <= i1 + (i - 1)
by A2, XREAL_1:9;
i1 + i <= i1 + ((((len f) -' 1) -' i1) + 1)
by A17, A22, XREAL_1:8;
then
i1 + i <= ((((len f) -' 1) - i1) + 1) + i1
by A6, XREAL_1:235;
then
i1 + i <= ((len f) -' 1) + 1
;
then
i1 + i <= len f
by A1, A2, XREAL_1:237, XXREAL_0:2;
then
(i1 + i) -' 1
<= (len f) - 1
by A20, XREAL_1:11;
then
( 1
<= (i1 + i) -' 1 &
(i1 + i) -' 1
<= (len f) -' 1 )
by A1, A2, A20, A25, XREAL_1:235, XXREAL_0:2;
hence
((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)
by A23, A24, Th34;
:: thesis: verum end; case A26:
i > len (mid f,i1,((len f) -' 1))
;
:: thesis: ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)A27:
(len f) - i1 = (len f) -' i1
by A1, XREAL_1:235;
i >= ((len f) -' i1) + 1
by A17, A18, A19, A26, NAT_1:13;
then A28:
i - ((len f) -' i1) >= (((len f) -' i1) + 1) - ((len f) -' i1)
by XREAL_1:11;
i - ((len f) - i1) <= (((len f) - i1) + i2) - ((len f) - i1)
by A14, A16, XREAL_1:11;
then A29:
( 1
<= i -' ((len f) -' i1) &
i -' ((len f) -' i1) <= i2 )
by A27, A28, NAT_D:39;
then A30:
i -' ((len f) -' i1) <= (len f) -' 1
by A8, XXREAL_0:2;
A31:
((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, A26, JORDAN3:15
.=
(mid f,1,i2) . (i -' ((len f) -' i1))
by A17, A18, A19, A26, XREAL_1:235
.=
f . (i -' ((len f) -' i1))
by A3, A29, JORDAN3:32
;
((len f) -' 1) + (i -' ((len f) -' i1)) =
((len f) -' 1) + (i - ((len f) -' i1))
by A17, A18, A19, A26, XREAL_1:235
.=
(((len f) -' 1) + i) - ((len f) -' i1)
.=
(((len f) - 1) + i) - ((len f) -' i1)
by A1, A2, XREAL_1:235, XXREAL_0:2
.=
(((len f) - 1) + i) - ((len f) - i1)
by A1, XREAL_1:235
.=
(i + i1) - 1
.=
(i1 + i) -' 1
by A16, NAT_D:37
;
then S_Drop ((i1 + i) -' 1),
f =
S_Drop (i -' ((len f) -' i1)),
f
by Th35
.=
i -' ((len f) -' i1)
by A29, A30, Th34
;
hence
((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)
by A31;
:: thesis: verum end;
hence
((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f)
;
:: thesis: verum
end;
hence
(mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,i1,i2
by A1, A2, A4, A5, A12, A13, A14, A15, Def2; :: thesis: verum