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 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 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 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 b1 being set holds
( not b1 in dom (Rotate (f,(N-min (L~ f)))) or b1 = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b1 = 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 b1 being set holds
( not b1 in dom (Rotate (f,(N-min (L~ f)))) or b1 = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b1 = 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 b1 being set holds
( not b1 in dom (Rotate (f,(N-min (L~ f)))) or b1 = (f /. 1) .. (Rotate (f,(N-min (L~ f)))) or not (Rotate (f,(N-min (L~ f)))) /. b1 = 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;