:: Rotating and reversing.(Finite sequences)
:: by Andrzej Trybulec
::
:: Copyright (c) 1999-2021 Association of Mizar Users

definition
end;

:: deftheorem REVROT_1:def 1 :
canceled;

:: deftheorem REVROT_1:def 2 :
canceled;

::$CD 2 theorem :: REVROT_1:1 canceled; ::$CD 2
theorem :: REVROT_1:2
canceled;

::$CD 2 theorem :: REVROT_1:3 canceled; ::$CD 2
theorem :: REVROT_1:4
canceled;

::$CD 2 theorem :: REVROT_1:5 canceled; ::$CD 2
theorem :: REVROT_1:6
canceled;

::$CD 2 theorem :: REVROT_1:7 canceled; ::$CD 2
theorem :: REVROT_1:8
canceled;

::$CD 2 theorem :: REVROT_1:9 canceled; ::$CD 2
theorem :: REVROT_1:10
canceled;

::$CD 2 theorem :: REVROT_1:11 canceled; ::$CD 2
theorem :: REVROT_1:12
canceled;

::$CD 2 theorem :: REVROT_1:13 canceled; ::$CD 2
theorem :: REVROT_1:14
canceled;

::$CD 2 theorem :: REVROT_1:15 canceled; ::$CD 2
theorem :: REVROT_1:16
canceled;

::$CD 2 theorem :: REVROT_1:17 canceled; ::$CD 2
theorem :: REVROT_1:18
canceled;

Th9: for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))

by FINSEQ_6:174;

Th10: for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds
f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

by FINSEQ_6:175;

Th11: for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

by FINSEQ_6:176;

Th14: for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Rotate (f,p)) = len f

by FINSEQ_6:179;

Th15: for D being non empty set
for p being Element of D
for f being FinSequence of D holds dom (Rotate (f,p)) = dom f

by FINSEQ_6:180;

Th16: for D being non empty set
for f being circular FinSequence of D
for p being Element of D st ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate ((Rotate (f,p)),(f /. 1)) = f

by FINSEQ_6:181;

Th17: for i being Nat
for D being non empty set
for p being Element of D
for f being circular 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))

by FINSEQ_6:182;

Th18: for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))

by FINSEQ_6:183;

theorem Th19: :: REVROT_1:19
for n being non zero Nat holds 0.REAL n <> 1.REAL n
proof end;

registration
let n be non zero Nat;
cluster TOP-REAL n -> non trivial ;
coherence
not TOP-REAL n is trivial
proof end;
end;

theorem Th20: :: REVROT_1:20
for f, g being FinSequence of () st rng f c= rng g holds
rng () c= rng ()
proof end;

theorem Th21: :: REVROT_1:21
for f, g being FinSequence of () st rng f = rng g holds
rng () = rng () by Th20;

theorem Th22: :: REVROT_1:22
for f, g being FinSequence of () st rng f c= rng g holds
rng () c= rng ()
proof end;

theorem Th23: :: REVROT_1:23
for f, g being FinSequence of () st rng f = rng g holds
rng () = rng () by Th22;

registration
let p be Point of ();
let f be circular special FinSequence of ();
cluster Rotate (f,p) -> special ;
coherence
Rotate (f,p) is special
proof end;
end;

theorem Th24: :: REVROT_1:24
for i being Nat
for p being Point of ()
for f being FinSequence of () st p in rng f & 1 <= i & i < len (f :- p) holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f)))
proof end;

theorem Th25: :: REVROT_1:25
for i being Nat
for p being Point of ()
for f being FinSequence of () st p in rng f & p .. f <= i & i < len f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1))
proof end;

theorem Th26: :: REVROT_1:26
for p being Point of ()
for f being circular FinSequence of () holds Incr () = Incr (X_axis (Rotate (f,p)))
proof end;

theorem Th27: :: REVROT_1:27
for p being Point of ()
for f being circular FinSequence of () holds Incr () = Incr (Y_axis (Rotate (f,p)))
proof end;

theorem Th28: :: REVROT_1:28
for p being Point of ()
for f being non empty circular FinSequence of () holds GoB (Rotate (f,p)) = GoB f
proof end;

theorem Th29: :: REVROT_1:29
for p being Point of ()
for f being V8() standard special_circular_sequence holds Rev (Rotate (f,p)) = Rotate ((Rev f),p)
proof end;

theorem Th30: :: REVROT_1:30
for f being circular s.c.c. FinSequence of () st len f > 4 holds
(LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)}
proof end;

theorem Th31: :: REVROT_1:31
for i being Nat
for p being Point of ()
for f being circular FinSequence of () st p in rng f & len (f :- p) <= i & i < len f holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))
proof end;

registration
let p be Point of ();
let f be circular s.c.c. FinSequence of ();
cluster Rotate (f,p) -> s.c.c. ;
coherence
Rotate (f,p) is s.c.c.
proof end;
end;

registration
let p be Point of ();
let f be V8() standard special_circular_sequence;
cluster Rotate (f,p) -> unfolded ;
coherence
Rotate (f,p) is unfolded
proof end;
end;

theorem Th32: :: REVROT_1:32
for i being Nat
for p being Point of ()
for f being circular FinSequence of () st p in rng f & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
proof end;

theorem Th33: :: REVROT_1:33
for p being Point of ()
for f being circular FinSequence of () holds L~ (Rotate (f,p)) = L~ f
proof end;

theorem Th34: :: REVROT_1:34
for p being Point of ()
for f being circular FinSequence of ()
for G being Go-board holds
( f is_sequence_on G iff Rotate (f,p) is_sequence_on G )
proof end;

registration
let p be Point of ();
let f be non empty circular standard FinSequence of ();
cluster Rotate (f,p) -> standard ;
coherence
Rotate (f,p) is standard
proof end;
end;

theorem Th35: :: REVROT_1:35
for f being V8() standard special_circular_sequence
for p being Point of ()
for k being Nat st p in rng f & 1 <= k & k < p .. f holds
left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f)))
proof end;

theorem Th36: :: REVROT_1:36
for p being Point of ()
for f being V8() standard special_circular_sequence holds LeftComp (Rotate (f,p)) = LeftComp f
proof end;

theorem :: REVROT_1:37
for p being Point of ()
for f being V8() standard special_circular_sequence holds RightComp (Rotate (f,p)) = RightComp f
proof end;

Lm1: for f being V8() standard special_circular_sequence holds
( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented )

proof end;

registration
let p be Point of ();
let f be V8() standard clockwise_oriented special_circular_sequence;
cluster Rotate (f,p) -> clockwise_oriented ;
coherence
Rotate (f,p) is clockwise_oriented
proof end;
end;

theorem :: REVROT_1:38
for f being V8() standard special_circular_sequence holds
( f is clockwise_oriented or Rev f is clockwise_oriented )
proof end;