let D be non empty set ; for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,1) = Op-LeftShift s
let s be FinSequence of D; ( 1 <= len s implies Op-Shift (s,1) = Op-LeftShift s )
assume A1:
1 <= len s
; Op-Shift (s,1) = Op-LeftShift s
A2:
( len (Op-Shift (s,1)) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) ) )
by Def3, A1;
A3:
( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s )
by A1, Th5;
A4:
len <*(s . 1)*> = 1
by FINSEQ_1:40;
A5:
len (s /^ 1) = (len s) - 1
by A1, RFINSEQ:def 1;
now for i being Nat st i in dom (Op-Shift (s,1)) holds
(Op-Shift (s,1)) . i = (Op-LeftShift s) . ilet i be
Nat;
( i in dom (Op-Shift (s,1)) implies (Op-Shift (s,1)) . i = (Op-LeftShift s) . i )assume
i in dom (Op-Shift (s,1))
;
(Op-Shift (s,1)) . i = (Op-LeftShift s) . ithen A6:
i in Seg (len s)
by A2, FINSEQ_1:def 3;
then A7:
( 1
<= i &
i <= len s )
by FINSEQ_1:1;
now (Op-Shift (s,1)) . i = (Op-LeftShift s) . iper cases
( i = len s or i <> len s )
;
suppose A8:
i = len s
;
(Op-Shift (s,1)) . i = (Op-LeftShift s) . iA9:
(Op-Shift (s,1)) . i =
s . ((((i - 1) + 1) mod (len s)) + 1)
by A6, Def3, A1
.=
s . (0 + 1)
by A1, A8, INT_1:62
.=
s . 1
;
A10:
i <= (len (s /^ 1)) + (len <*(s . 1)*>)
by A8, A5, A4;
A11:
i - (len (s /^ 1)) = (len s) - ((len s) - 1)
by A8, A1, RFINSEQ:def 1;
(Op-LeftShift s) . i =
<*(s . 1)*> . 1
by A10, A4, A11, FINSEQ_1:23
.=
s . 1
by FINSEQ_1:40
;
hence
(Op-Shift (s,1)) . i = (Op-LeftShift s) . i
by A9;
verum end; suppose
i <> len s
;
(Op-Shift (s,1)) . i = (Op-LeftShift s) . ithen A12:
(
0 <= i &
i < len s )
by A7, XXREAL_0:1;
i + 1
<= len s
by A12, NAT_1:13;
then A13:
(i + 1) - 1
<= (len s) - 1
by XREAL_1:9;
then A14:
( 1
<= i &
i <= (len s) - 1 )
by A6, FINSEQ_1:1;
reconsider ls1 =
(len s) - 1 as
Element of
NAT by A13, INT_1:3;
i in Seg ls1
by A14;
then A15:
i in dom (s /^ 1)
by A5, FINSEQ_1:def 3;
A16:
(Op-Shift (s,1)) . i =
s . ((((i - 1) + 1) mod (len s)) + 1)
by A6, Def3, A1
.=
s . (i + 1)
by A12, NAT_D:63
;
(Op-LeftShift s) . i =
(s /^ 1) . i
by A5, A14, FINSEQ_1:64
.=
s . (i + 1)
by A15, A1, RFINSEQ:def 1
;
hence
(Op-Shift (s,1)) . i = (Op-LeftShift s) . i
by A16;
verum end; end; end; hence
(Op-Shift (s,1)) . i = (Op-LeftShift s) . i
;
verum end;
hence
Op-Shift (s,1) = Op-LeftShift s
by A2, A3, FINSEQ_2:9; verum