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: N-min (L~ f) in rng f by SPRECT_2:43;
L~ f = L~ (Rotate f,(N-min (L~ f))) by Th33;
then A3: (Rotate f,(N-min (L~ f))) /. 1 = N-min (L~ (Rotate f,(N-min (L~ f)))) by A2, FINSEQ_6:98;
A4: for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:38;
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 ;
A5: 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 ) )
A6: N-min (L~ f) in rng f by SPRECT_2:43;
f /. 1 in rng f by FINSEQ_6:46;
then A7: f /. 1 in rng (Rotate f,(N-min (L~ f))) by FINSEQ_6:96, SPRECT_2:43;
A8: f /. 1 <> (Rotate f,(N-min (L~ f))) /. 1 by A1, A6, FINSEQ_6:98;
thus A9: (f /. 1) .. (Rotate f,(N-min (L~ f))) in dom (Rotate f,(N-min (L~ f))) by A7, 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 A10: f /. 1 = (Rotate f,(N-min (L~ f))) . ((f /. 1) .. (Rotate f,(N-min (L~ f)))) by A7, FINSEQ_4:29
.= (Rotate f,(N-min (L~ f))) /. ((f /. 1) .. (Rotate f,(N-min (L~ f)))) by A9, 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
A11: z in dom (Rotate f,(N-min (L~ f))) and
A12: 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 A11;
per cases ( k < (f /. 1) .. (Rotate f,(N-min (L~ f))) or k > (f /. 1) .. (Rotate f,(N-min (L~ f))) ) by A12, XXREAL_0:1;
suppose A13: k < (f /. 1) .. (Rotate f,(N-min (L~ f))) ; :: thesis: (Rotate f,(N-min (L~ f))) /. z <> f /. 1
A14: (f /. 1) .. (Rotate f,(N-min (L~ f))) <= len (Rotate f,(N-min (L~ f))) by A7, FINSEQ_4:31;
(f /. 1) .. (Rotate f,(N-min (L~ f))) <> len (Rotate f,(N-min (L~ f))) by A8, A10, FINSEQ_6:def 1;
then A15: (f /. 1) .. (Rotate f,(N-min (L~ f))) < len (Rotate f,(N-min (L~ f))) by A14, XXREAL_0:1;
1 <= k by A11, FINSEQ_3:27;
hence (Rotate f,(N-min (L~ f))) /. z <> f /. 1 by A10, A13, A15, GOBOARD7:38; :: thesis: verum
end;
suppose A16: 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 A7, FINSEQ_4:31;
then A17: (f /. 1) .. (Rotate f,(N-min (L~ f))) > 1 by A8, A10, XXREAL_0:1;
k <= len (Rotate f,(N-min (L~ f))) by A11, FINSEQ_3:27;
hence (Rotate f,(N-min (L~ f))) /. z <> f /. 1 by A10, A16, A17, GOBOARD7:39; :: thesis: verum
end;
end;
end;
Rev f = Rev (Rotate (Rotate f,(N-min (L~ f))),(f /. 1)) by A4, Th16
.= Rotate h,(f /. 1) by A5, FINSEQ_6:112 ;
hence ( f is clockwise_oriented or Rev f is clockwise_oriented ) ; :: thesis: verum
end;
end;
end;
end;
end;