let f be V8() 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 Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:38;
( N-min (L~ f) in rng f & L~ f = L~ (Rotate f,(N-min (L~ f))) ) by Th33, SPRECT_2:43;
then A3: (Rotate f,(N-min (L~ f))) /. 1 = N-min (L~ (Rotate f,(N-min (L~ f)))) by FINSEQ_6:98;
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 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 V8() 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 REVROT_1:def 2 :: 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 z being set st z in dom (Rotate f,(N-min (L~ f))) & z <> (f /. 1) .. (Rotate f,(N-min (L~ f))) holds
(Rotate f,(N-min (L~ f))) /. z <> f /. 1 ) )
N-min (L~ f) in rng f by SPRECT_2:43;
then A5: f /. 1 <> (Rotate f,(N-min (L~ f))) /. 1 by A1, FINSEQ_6:98;
f /. 1 in rng f by FINSEQ_6:46;
then A6: f /. 1 in rng (Rotate f,(N-min (L~ f))) by FINSEQ_6:96, SPRECT_2:43;
hence A7: (f /. 1) .. (Rotate f,(N-min (L~ f))) in dom (Rotate f,(N-min (L~ f))) by FINSEQ_4:30; :: thesis: ( f /. 1 = (Rotate f,(N-min (L~ f))) /. ((f /. 1) .. (Rotate f,(N-min (L~ f)))) & ( for z being set st z in dom (Rotate f,(N-min (L~ f))) & z <> (f /. 1) .. (Rotate f,(N-min (L~ f))) holds
(Rotate f,(N-min (L~ f))) /. z <> f /. 1 ) )
thus A8: f /. 1 = (Rotate f,(N-min (L~ f))) . ((f /. 1) .. (Rotate f,(N-min (L~ f)))) by A6, FINSEQ_4:29
.= (Rotate f,(N-min (L~ f))) /. ((f /. 1) .. (Rotate f,(N-min (L~ f)))) by A7, PARTFUN1:def 8 ; :: thesis: for z being set st z in dom (Rotate f,(N-min (L~ f))) & z <> (f /. 1) .. (Rotate f,(N-min (L~ f))) holds
(Rotate f,(N-min (L~ f))) /. z <> f /. 1
let z be set ; :: thesis: ( z in dom (Rotate f,(N-min (L~ f))) & z <> (f /. 1) .. (Rotate f,(N-min (L~ f))) implies (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: (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: (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:31, 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:27;
hence (Rotate f,(N-min (L~ f))) /. z <> f /. 1 by A8, A11, A12, GOBOARD7:38; :: thesis: verum
end;
suppose A13: k > (f /. 1) .. (Rotate f,(N-min (L~ f))) ; :: thesis: (Rotate f,(N-min (L~ f))) /. z <> f /. 1
(f /. 1) .. (Rotate f,(N-min (L~ f))) >= 1 by A6, FINSEQ_4:31;
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:27;
hence (Rotate f,(N-min (L~ f))) /. z <> f /. 1 by A8, A13, A14, GOBOARD7:39; :: 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:112 ;
hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; :: thesis: verum
end;
end;
end;
end;
end;