let i be Nat; for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
let D be non empty set ; for p being Element of D
for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
let p be Element of D; for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
let f be FinSequence of D; ( p in rng f & len (f :- p) < i & i <= len f implies (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) )
assume that
A1:
p in rng f
and
A2:
len (f :- p) < i
and
A3:
i <= len f
; (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
A4:
len (f -: p) = p .. f
by A1, FINSEQ_5:42;
A5:
( (i -' (len (f :- p))) + (len (f :- p)) = i & Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) )
by A1, A2, Def2, XREAL_1:235;
not f -: p is empty
by A1, FINSEQ_5:47;
then
len (f -: p) >= 1
by NAT_1:14;
then A6:
len ((f -: p) /^ 1) = (len (f -: p)) - 1
by RFINSEQ:def 1;
i + (p .. f) <= (p .. f) + (len f)
by A3, XREAL_1:6;
then A7:
(i + (p .. f)) -' (len f) <= p .. f
by NAT_D:53;
A8:
p .. f <= len f
by A1, FINSEQ_4:21;
then
(len f) - (p .. f) = (len f) -' (p .. f)
by XREAL_1:233;
then A9:
len (f :- p) = ((len f) -' (p .. f)) + 1
by A1, FINSEQ_5:50;
then A10:
(len f) -' (p .. f) < i
by A2, NAT_1:13;
then A11:
len f < i + (p .. f)
by NAT_D:55;
then
(len f) + 1 <= i + (p .. f)
by NAT_1:13;
then
1 <= (i + (p .. f)) -' (len f)
by NAT_D:55;
then A12:
(i + (p .. f)) -' (len f) in Seg (p .. f)
by A7;
i <= (p .. f) + ((len f) -' (p .. f))
by A3, A8, XREAL_1:235;
then
i -' ((len f) -' (p .. f)) <= p .. f
by NAT_D:53;
then
(i -' (((len f) -' (p .. f)) + 1)) + 1 <= p .. f
by A10, NAT27;
then A13:
i -' (len (f :- p)) <= (len (f -: p)) - 1
by A9, A4, XREAL_1:19;
(((len f) -' (p .. f)) + 1) + 1 <= i
by A2, A9, NAT_1:13;
then A14:
1 <= i -' (((len f) -' (p .. f)) + 1)
by NAT_D:55;
then A15:
i -' (((len f) -' (p .. f)) + 1) in dom ((f -: p) /^ 1)
by A9, A6, A13, FINSEQ_3:25;
(len f) - (p .. f) = (len f) -' (p .. f)
by A8, XREAL_1:233;
then
1 <= i -' (len (f :- p))
by A1, A14, FINSEQ_5:50;
then
i -' (len (f :- p)) in dom ((f -: p) /^ 1)
by A6, A13, FINSEQ_3:25;
hence (Rotate (f,p)) /. i =
((f -: p) /^ 1) /. (i -' (((len f) -' (p .. f)) + 1))
by A9, A5, FINSEQ_4:69
.=
(f -: p) /. ((i -' (((len f) -' (p .. f)) + 1)) + 1)
by A15, FINSEQ_5:27
.=
(f -: p) /. (i -' ((len f) -' (p .. f)))
by A10, NAT27
.=
(f -: p) /. (i - ((len f) -' (p .. f)))
by A10, XREAL_1:233
.=
(f -: p) /. (i - ((len f) - (p .. f)))
by A8, XREAL_1:233
.=
(f -: p) /. ((i + (p .. f)) - (len f))
.=
(f -: p) /. ((i + (p .. f)) -' (len f))
by A11, XREAL_1:233
.=
f /. ((i + (p .. f)) -' (len f))
by A1, A12, FINSEQ_5:43
;
verum