let f be constant standard special_circular_sequence; :: thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented )

per cases ( N-min (L~ f) = f /. 1 or N-min (L~ f) <> f /. 1 ) ;

suppose N-min (L~ f) = f /. 1 ; :: thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented )

hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) by Lm1; :: thesis: verum

end;

suppose A1: N-min (L~ f) <> f /. 1 ; :: thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented )

thus ( f is clockwise_oriented or Rev f is clockwise_oriented ) :: thesis: verum

proof

set g = Rotate (f,(N-min (L~ f)));
A2: for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:36;
( N-min (L~ f) in rng f & L~ f = L~ (Rotate (f,(N-min (L~ f)))) ) by Th33, SPRECT_2:39;
then A3: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by FINSEQ_6:92;

per cases ( Rotate (f,(N-min (L~ f))) is clockwise_oriented or Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented ) by A3, Lm1;

suppose Rotate (f,(N-min (L~ f))) is clockwise_oriented ; :: thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented )

then reconsider g = Rotate (f,(N-min (L~ f))) as constant standard clockwise_oriented special_circular_sequence ;
f = Rotate (g,(f /. 1)) by A2, Th16;
hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; :: thesis: verum

end;

suppose Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented ; :: thesis: ( f is clockwise_oriented or Rev f is clockwise_oriented )

then reconsider h = Rev (Rotate (f,(N-min (L~ f)))) as constant standard clockwise_oriented special_circular_sequence ;
A4: Rotate (f,(N-min (L~ f))) just_once_values f /. 1

proof

take (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; :: according to FINSEQ_6:def 12 :: thesis: ( (f /. 1) .. (Rotate (f,(N-min (L~ f)))) in dom (Rotate (f,(N-min (L~ f)))) & f /. 1 = (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) & ( for b₁ being set holds
( not b₁ in dom (Rotate (f,(N-min (L~ f)))) or b₁ = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b₁ = f /. 1 ) ) )
N-min (L~ f) in rng f by SPRECT_2:39;
then A5: f /. 1 <> (Rotate (f,(N-min (L~ f)))) /. 1 by A1, FINSEQ_6:92;
f /. 1 in rng f by FINSEQ_6:42;
then A6: f /. 1 in rng (Rotate (f,(N-min (L~ f)))) by FINSEQ_6:90, SPRECT_2:39;
hence A7: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) in dom (Rotate (f,(N-min (L~ f)))) by FINSEQ_4:20; :: thesis: ( f /. 1 = (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) & ( for b₁ being set holds
( not b₁ in dom (Rotate (f,(N-min (L~ f)))) or b₁ = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b₁ = f /. 1 ) ) )
thus A8: f /. 1 = (Rotate (f,(N-min (L~ f)))) . ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) by A6, FINSEQ_4:19
.= (Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) by A7, PARTFUN1:def 6 ; :: thesis: for b₁ being set holds
( not b₁ in dom (Rotate (f,(N-min (L~ f)))) or b₁ = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b₁ = f /. 1 )
let z be set ; :: thesis: ( not z in dom (Rotate (f,(N-min (L~ f)))) or z = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1 )
assume that
A9: z in dom (Rotate (f,(N-min (L~ f)))) and
A10: z <> (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; :: thesis: not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1
reconsider k = z as Element of NAT by A9;

per cases ( k < (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or k > (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ) by A10, XXREAL_0:1;

suppose A11: k < (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; :: thesis: not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1

( (f /. 1) .. (Rotate (f,(N-min (L~ f)))) <= len (Rotate (f,(N-min (L~ f)))) & (f /. 1) .. (Rotate (f,(N-min (L~ f)))) <> len (Rotate (f,(N-min (L~ f)))) ) by A6, A5, A8, FINSEQ_4:21, FINSEQ_6:def 1;
then A12: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) < len (Rotate (f,(N-min (L~ f)))) by XXREAL_0:1;
1 <= k by A9, FINSEQ_3:25;
hence not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1 by A8, A11, A12, GOBOARD7:36; :: thesis: verum

end;

suppose A13: k > (f /. 1) .. (Rotate (f,(N-min (L~ f)))) ; :: thesis: not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1

(f /. 1) .. (Rotate (f,(N-min (L~ f)))) >= 1 by A6, FINSEQ_4:21;
then A14: (f /. 1) .. (Rotate (f,(N-min (L~ f)))) > 1 by A5, A8, XXREAL_0:1;
k <= len (Rotate (f,(N-min (L~ f)))) by A9, FINSEQ_3:25;
hence not (Rotate (f,(N-min (L~ f)))) /. z = f /. 1 by A8, A13, A14, GOBOARD7:37; :: thesis: verum

end;

end;

end;

Rev f = Rev (Rotate ((Rotate (f,(N-min (L~ f)))),(f /. 1))) by A2, Th16
.= Rotate (h,(f /. 1)) by A4, FINSEQ_6:106 ;
hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; :: thesis: verum

end;

end;

end;

end;

end;