:: Rotating and reversing.(Finite sequences)
:: by Andrzej Trybulec
::
:: Received January 21, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem Def1 defines constant REVROT_1:def 1 :
theorem Th1: :: REVROT_1:1
theorem :: REVROT_1:2
theorem Th3: :: REVROT_1:3
:: deftheorem defines just_once_values REVROT_1:def 2 :
theorem Th4: :: REVROT_1:4
theorem Th5: :: REVROT_1:5
theorem Th6: :: REVROT_1:6
theorem :: REVROT_1:7
theorem :: REVROT_1:8
theorem Th9: :: REVROT_1:9
theorem Th10: :: REVROT_1:10
theorem Th11: :: REVROT_1:11
theorem Th12: :: REVROT_1:12
theorem :: REVROT_1:13
theorem Th14: :: REVROT_1:14
theorem Th15: :: REVROT_1:15
theorem Th16: :: REVROT_1:16
theorem Th17: :: REVROT_1:17
theorem Th18: :: REVROT_1:18
theorem Th19: :: REVROT_1:19
theorem Th20: :: REVROT_1:20
theorem Th21: :: REVROT_1:21
theorem Th22: :: REVROT_1:22
theorem Th23: :: REVROT_1:23
theorem Th24: :: REVROT_1:24
theorem Th25: :: REVROT_1:25
theorem Th26: :: REVROT_1:26
theorem Th27: :: REVROT_1:27
theorem Th28: :: REVROT_1:28
theorem Th29: :: REVROT_1:29
theorem Th30: :: REVROT_1:30
theorem Th31: :: REVROT_1:31
theorem Th32: :: REVROT_1:32
theorem Th33: :: REVROT_1:33
theorem Th34: :: REVROT_1:34
theorem Th35: :: REVROT_1:35
theorem Th36: :: REVROT_1:36
theorem :: REVROT_1:37
Lm1:
for f being V6 standard special_circular_sequence holds
( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented )
theorem :: REVROT_1:38