let D be non empty set ; for f being FinSequence of D
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))
let f be FinSequence of D; for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))
let k1, k2 be Nat; ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f implies Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) )
assume that
A1:
1 <= k1
and
A2:
k1 <= len f
and
A3:
1 <= k2
and
A4:
k2 <= len f
; Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))
per cases
( k1 <= k2 or k1 > k2 )
;
suppose A5:
k1 <= k2
;
Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))A6:
(len f) -' (k1 -' 1) =
(len f) - (k1 -' 1)
by A2, NAT_D:50, XREAL_1:233
.=
(len f) - (k1 - 1)
by A1, XREAL_1:233
.=
((len f) - k1) + 1
.=
((len f) -' k1) + 1
by A2, XREAL_1:233
;
A7:
(len f) -' k1 = (len f) - k1
by A2, XREAL_1:233;
A8:
(len f) -' k2 = (len f) - k2
by A4, XREAL_1:233;
k2 - k1 <= (len f) - k1
by A4, XREAL_1:9;
then
k2 -' k1 <= (len f) - k1
by A5, XREAL_1:233;
then
k2 -' k1 <= (len f) -' k1
by A2, XREAL_1:233;
then
(k2 -' k1) + 1
<= ((len f) -' k1) + 1
by XREAL_1:6;
then A9:
((len f) -' (k1 -' 1)) -' ((k2 -' k1) + 1) =
(((len f) -' k1) + 1) - ((k2 -' k1) + 1)
by A6, XREAL_1:233
.=
(((len f) - k1) + 1) - ((k2 - k1) + 1)
by A5, A7, XREAL_1:233
.=
(((len f) + 1) - 1) - k2
.=
(len f) -' k2
by A4, XREAL_1:233
;
then A10:
((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) + ((k2 -' k1) + 1) =
((len f) -' k2) + ((k2 -' k1) + 1)
by RFINSEQ:29
.=
((len f) - k2) + ((k2 - k1) + 1)
by A5, A8, XREAL_1:233
.=
(len f) - (k1 - 1)
.=
(len f) - (k1 -' 1)
by A1, XREAL_1:233
.=
(len f) -' (k1 -' 1)
by A2, NAT_D:50, XREAL_1:233
.=
len (f /^ (k1 -' 1))
by RFINSEQ:29
;
A11:
(len f) -' k1 <= ((len f) -' k1) + 1
by NAT_1:11;
(len f) -' k1 >= (len f) -' k2
by A5, NAT_D:41;
then A12:
((len f) -' (k1 -' 1)) -' ((len f) -' k2) =
(((len f) -' k1) + 1) - ((len f) -' k2)
by A6, A11, XREAL_1:233, XXREAL_0:2
.=
(((len f) - k1) + 1) - ((len f) - k2)
by A4, A7, XREAL_1:233
.=
(k2 - k1) + 1
.=
(k2 -' k1) + 1
by A5, XREAL_1:233
;
A13:
((len f) -' (k1 -' 1)) + (k1 -' 1) =
((len f) - (k1 -' 1)) + (k1 -' 1)
by A2, NAT_D:50, XREAL_1:233
.=
len f
;
(len f) -' k1 >= (len f) -' k2
by A5, NAT_D:41;
then
((len f) -' k1) + 1
>= ((len f) -' k2) + 1
by XREAL_1:6;
then A14:
((((len f) -' k1) + 1) -' (((len f) -' k2) + 1)) + 1 =
((((len f) -' k1) + 1) - (((len f) -' k2) + 1)) + 1
by XREAL_1:233
.=
((((len f) - k1) + 1) - (((len f) - k2) + 1)) + 1
by A4, A7, XREAL_1:233
.=
(k2 - k1) + 1
.=
(k2 -' k1) + 1
by A5, XREAL_1:233
;
(len f) -' k1 >= (len f) -' k2
by A5, NAT_D:41;
then
((len f) -' k1) + 1
>= ((len f) -' k2) + 1
by XREAL_1:6;
then mid (
(Rev f),
(((len f) -' k2) + 1),
(((len f) -' k1) + 1)) =
((Rev f) /^ ((((len f) -' k2) + 1) -' 1)) | ((k2 -' k1) + 1)
by A14, Def3
.=
((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2))
by A12, NAT_D:34
.=
((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len f) -' k2)
by FINSEQ_5:80
.=
((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1))
by A9, RFINSEQ:29
.=
(Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1))
by A13, Th84
.=
Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1))
by A10, Th85
.=
Rev (mid (f,k1,k2))
by A5, Def3
;
hence
Rev (mid (f,k1,k2)) = mid (
(Rev f),
(((len f) -' k2) + 1),
(((len f) -' k1) + 1))
;
verum end; suppose A15:
k1 > k2
;
Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))A16:
(len f) -' (k2 -' 1) =
(len f) - (k2 -' 1)
by A4, NAT_D:50, XREAL_1:233
.=
(len f) - (k2 - 1)
by A3, XREAL_1:233
.=
((len f) - k2) + 1
.=
((len f) -' k2) + 1
by A4, XREAL_1:233
;
A17:
(len f) -' k2 = (len f) - k2
by A4, XREAL_1:233;
(len f) -' k2 >= (len f) -' k1
by A15, NAT_D:41;
then
((len f) -' k2) + 1
>= ((len f) -' k1) + 1
by XREAL_1:6;
then A18:
((((len f) -' k2) + 1) -' (((len f) -' k1) + 1)) + 1 =
((((len f) -' k2) + 1) - (((len f) -' k1) + 1)) + 1
by XREAL_1:233
.=
((((len f) - k2) + 1) - (((len f) - k1) + 1)) + 1
by A2, A17, XREAL_1:233
.=
(k1 - k2) + 1
.=
(k1 -' k2) + 1
by A15, XREAL_1:233
;
A19:
(len f) -' k1 = (len f) - k1
by A2, XREAL_1:233;
A20:
(len f) -' k2 <= ((len f) -' k2) + 1
by NAT_1:11;
(len f) -' k2 >= (len f) -' k1
by A15, NAT_D:41;
then A21:
((len f) -' (k2 -' 1)) -' ((len f) -' k1) =
(((len f) -' k2) + 1) - ((len f) -' k1)
by A16, A20, XREAL_1:233, XXREAL_0:2
.=
(((len f) - k2) + 1) - ((len f) - k1)
by A2, A17, XREAL_1:233
.=
(k1 - k2) + 1
.=
(k1 -' k2) + 1
by A15, XREAL_1:233
;
A22:
((len f) -' (k2 -' 1)) + (k2 -' 1) =
((len f) - (k2 -' 1)) + (k2 -' 1)
by A4, NAT_D:50, XREAL_1:233
.=
len f
;
k1 - k2 <= (len f) - k2
by A2, XREAL_1:9;
then
k1 -' k2 <= (len f) - k2
by A15, XREAL_1:233;
then
k1 -' k2 <= (len f) -' k2
by A4, XREAL_1:233;
then
(k1 -' k2) + 1
<= ((len f) -' k2) + 1
by XREAL_1:6;
then A23:
((len f) -' (k2 -' 1)) -' ((k1 -' k2) + 1) =
(((len f) -' k2) + 1) - ((k1 -' k2) + 1)
by A16, XREAL_1:233
.=
(((len f) - k2) + 1) - ((k1 - k2) + 1)
by A15, A17, XREAL_1:233
.=
(((len f) + 1) - 1) - k1
.=
(len f) -' k1
by A2, XREAL_1:233
;
then A24:
((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) + ((k1 -' k2) + 1) =
((len f) -' k1) + ((k1 -' k2) + 1)
by RFINSEQ:29
.=
((len f) - k1) + ((k1 - k2) + 1)
by A15, A19, XREAL_1:233
.=
(len f) - (k2 - 1)
.=
(len f) - (k2 -' 1)
by A3, XREAL_1:233
.=
(len f) -' (k2 -' 1)
by A4, NAT_D:50, XREAL_1:233
.=
len (f /^ (k2 -' 1))
by RFINSEQ:29
;
(len f) - k2 > (len f) - k1
by A15, XREAL_1:10;
then
((len f) -' k2) + 1
> ((len f) -' k1) + 1
by A17, A19, XREAL_1:6;
then mid (
(Rev f),
(((len f) -' k2) + 1),
(((len f) -' k1) + 1)) =
Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1))
by A18, Def3
.=
Rev (((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1)))
by A21, NAT_D:34
.=
Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len f) -' k1))
by FINSEQ_5:80
.=
Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)))
by A23, RFINSEQ:29
.=
Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)))
by A22, Th84
.=
Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)))
by A24, Th85
.=
Rev (mid (f,k1,k2))
by A15, Def3
;
hence
Rev (mid (f,k1,k2)) = mid (
(Rev f),
(((len f) -' k2) + 1),
(((len f) -' k1) + 1))
;
verum end;