revrot_1.miz



    begin

    reserve i,j,k,m,n for Nat,

D for non empty set,

p for Element of D,

f for FinSequence of D;

    definition

      ::$Canceled

    end

    ::$Canceled

    reserve D for non empty set,

p for Element of D,

f for FinSequence of D;

    

     Th9: p in ( rng f) & 1 <= i & i <= ( len (f :- p)) implies (( Rotate (f,p)) /. i) = (f /. ((i -' 1) + (p .. f))) by FINSEQ_6: 174;

    

     Th10: p in ( rng f) & (p .. f) <= i & i <= ( len f) implies (f /. i) = (( Rotate (f,p)) /. ((i + 1) -' (p .. f))) by FINSEQ_6: 175;

    

     Th11: p in ( rng f) implies (( Rotate (f,p)) /. ( len (f :- p))) = (f /. ( len f)) by FINSEQ_6: 176;

    

     Th14: ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

    

     Th15: ( dom ( Rotate (f,p))) = ( dom f) by FINSEQ_6: 180;

    

     Th16: for D be non empty set, f be circular FinSequence of D, p be Element of D st for i st 1 < i & i < ( len f) holds (f /. i) <> (f /. 1) holds ( Rotate (( Rotate (f,p)),(f /. 1))) = f by FINSEQ_6: 181;

    begin

    reserve f for circular FinSequence of D;

    

     Th17: p in ( rng f) & ( len (f :- p)) <= i & i <= ( len f) implies (( Rotate (f,p)) /. i) = (f /. ((i + (p .. f)) -' ( len f))) by FINSEQ_6: 182;

    

     Th18: p in ( rng f) & 1 <= i & i <= (p .. f) implies (f /. i) = (( Rotate (f,p)) /. ((i + ( len f)) -' (p .. f))) by FINSEQ_6: 183;

    begin

    theorem :: REVROT_1:19

    

     Th19: for n be non zero Nat holds ( 0.REAL n) <> ( 1.REAL n)

    proof

      let n be non zero Nat;

      1 <= n by NAT_1: 14;

      then 1 in ( Seg n) by FINSEQ_1: 1;

      then

       A1: ((n |-> 0 ) . 1) = 0 & ((n |-> 1) . 1) = 1 by FINSEQ_2: 57;

      ( 1.REAL n) = ( 1* n) by EUCLID:def 12

      .= (n |-> 1) by EUCLID:def 11;

      hence thesis by A1, EUCLID:def 4;

    end;

    registration

      let n be non zero Nat;

      cluster ( TOP-REAL n) -> non trivial;

      coherence

      proof

        reconsider 1R = ( 1.REAL n) as Element of ( TOP-REAL n);

        take 1R;

        ( 0.REAL n) = ( 0. ( TOP-REAL n)) by EUCLID: 66;

        hence 1R <> ( 0. ( TOP-REAL n)) by Th19;

      end;

    end

    reserve f,g for FinSequence of ( TOP-REAL 2);

    theorem :: REVROT_1:20

    

     Th20: ( rng f) c= ( rng g) implies ( rng ( X_axis f)) c= ( rng ( X_axis g))

    proof

      assume

       A1: ( rng f) c= ( rng g);

      

       A2: ( dom ( X_axis g)) = ( dom g) by SPRECT_2: 15;

      let x be object;

      assume x in ( rng ( X_axis f));

      then

      consider y be object such that

       A3: y in ( dom ( X_axis f)) and

       A4: (( X_axis f) . y) = x by FUNCT_1:def 3;

      reconsider y as Element of NAT by A3;

      

       A5: (( X_axis f) . y) = ((f /. y) `1 ) by A3, GOBOARD1:def 1;

      ( dom ( X_axis f)) = ( dom f) by SPRECT_2: 15;

      then (f /. y) in ( rng f) by A3, PARTFUN2: 2;

      then

      consider z be object such that

       A6: z in ( dom g) and

       A7: (g . z) = (f /. y) by A1, FUNCT_1:def 3;

      reconsider z as Element of NAT by A6;

      (g /. z) = (f /. y) by A6, A7, PARTFUN1:def 6;

      then (( X_axis g) . z) = ((f /. y) `1 ) by A2, A6, GOBOARD1:def 1;

      hence thesis by A4, A2, A5, A6, FUNCT_1:def 3;

    end;

    theorem :: REVROT_1:21

    

     Th21: ( rng f) = ( rng g) implies ( rng ( X_axis f)) = ( rng ( X_axis g)) by Th20;

    theorem :: REVROT_1:22

    

     Th22: ( rng f) c= ( rng g) implies ( rng ( Y_axis f)) c= ( rng ( Y_axis g))

    proof

      assume

       A1: ( rng f) c= ( rng g);

      

       A2: ( dom ( Y_axis g)) = ( dom g) by SPRECT_2: 16;

      let x be object;

      assume x in ( rng ( Y_axis f));

      then

      consider y be object such that

       A3: y in ( dom ( Y_axis f)) and

       A4: (( Y_axis f) . y) = x by FUNCT_1:def 3;

      reconsider y as Element of NAT by A3;

      

       A5: (( Y_axis f) . y) = ((f /. y) `2 ) by A3, GOBOARD1:def 2;

      ( dom ( Y_axis f)) = ( dom f) by SPRECT_2: 16;

      then (f /. y) in ( rng f) by A3, PARTFUN2: 2;

      then

      consider z be object such that

       A6: z in ( dom g) and

       A7: (g . z) = (f /. y) by A1, FUNCT_1:def 3;

      reconsider z as Element of NAT by A6;

      (g /. z) = (f /. y) by A6, A7, PARTFUN1:def 6;

      then (( Y_axis g) . z) = ((f /. y) `2 ) by A2, A6, GOBOARD1:def 2;

      hence thesis by A4, A2, A5, A6, FUNCT_1:def 3;

    end;

    theorem :: REVROT_1:23

    

     Th23: ( rng f) = ( rng g) implies ( rng ( Y_axis f)) = ( rng ( Y_axis g)) by Th22;

    begin

    reserve p for Point of ( TOP-REAL 2),

f for FinSequence of ( TOP-REAL 2);

    registration

      let p be Point of ( TOP-REAL 2);

      let f be special circular FinSequence of ( TOP-REAL 2);

      cluster ( Rotate (f,p)) -> special;

      coherence

      proof

        per cases ;

          suppose not p in ( rng f);

          hence thesis by FINSEQ_6:def 2;

        end;

          suppose

           A1: p in ( rng f);

          

           A2: ( len ( Rotate (f,p))) = ( len f) by Th14;

          let i be Nat such that

           A3: 1 <= i and

           A4: (i + 1) <= ( len ( Rotate (f,p)));

          

           A5: (i + 1) >= i by NAT_1: 11;

          now

            

             A6: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

            per cases ;

              suppose

               A7: i < ( len (f :- p));

              

               A8: (((i + 1) -' 1) + (p .. f)) = (i + (p .. f)) by NAT_D: 34

              .= (((i -' 1) + 1) + (p .. f)) by A3, XREAL_1: 235

              .= (((i -' 1) + (p .. f)) + 1);

              (i + 1) <= ( len (f :- p)) by A7, NAT_1: 13;

              then

               A9: (( Rotate (f,p)) /. (i + 1)) = (f /. (((i -' 1) + (p .. f)) + 1)) by A1, A8, Th9, NAT_1: 11;

               0 <= (i -' 1) & 1 <= (p .. f) by A1, FINSEQ_4: 21;

              then

               A10: (1 + 0 ) <= ((i -' 1) + (p .. f)) by XREAL_1: 7;

              i < ((( len f) + 1) - (p .. f)) by A6, A7;

              then (i + (p .. f)) < (( len f) + 1) by XREAL_1: 20;

              then (i + (p .. f)) <= ( len f) by NAT_1: 13;

              then

               A11: (((i -' 1) + 1) + (p .. f)) <= ( len f) by A3, XREAL_1: 235;

              (( Rotate (f,p)) /. i) = (f /. ((i -' 1) + (p .. f))) by A1, A3, A7, Th9;

              hence thesis by A9, A10, A11, TOPREAL1:def 5;

            end;

              suppose

               A12: i >= ( len (f :- p));

              i <= ( len f) by A4, A5, A2, XXREAL_0: 2;

              then

               A13: (( Rotate (f,p)) /. i) = (f /. ((i + (p .. f)) -' ( len f))) by A1, A12, Th17;

              (i - (( len f) - (p .. f))) >= 1 by A6, A12, XREAL_1: 19;

              then ((i + (p .. f)) - ( len f)) >= 1;

              then

               A14: 1 <= ((i + (p .. f)) -' ( len f)) by NAT_D: 39;

              

               A15: (i + 1) >= ( len (f :- p)) by A5, A12, XXREAL_0: 2;

              then i >= (( len f) - (p .. f)) by A6, XREAL_1: 6;

              then

               A16: ( len f) <= (i + (p .. f)) by XREAL_1: 20;

              (((i + 1) + (p .. f)) -' ( len f)) = (((i + (p .. f)) + 1) -' ( len f))

              .= (((i + (p .. f)) -' ( len f)) + 1) by A16, NAT_D: 38;

              then

               A17: (( Rotate (f,p)) /. (i + 1)) = (f /. (((i + (p .. f)) -' ( len f)) + 1)) by A1, A4, A2, A15, Th17;

              (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

              then ((i + 1) + (p .. f)) <= (( len f) + ( len f)) by A4, A2, XREAL_1: 7;

              then (((i + (p .. f)) + 1) - ( len f)) <= ( len f) by XREAL_1: 20;

              then (((i + (p .. f)) - ( len f)) + 1) <= ( len f);

              then (((i + (p .. f)) -' ( len f)) + 1) <= ( len f) by A16, XREAL_1: 233;

              hence thesis by A13, A17, A14, TOPREAL1:def 5;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: REVROT_1:24

    

     Th24: p in ( rng f) & 1 <= i & i < ( len (f :- p)) implies ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i -' 1) + (p .. f))))

    proof

      assume that

       A1: p in ( rng f) and

       A2: 1 <= i and

       A3: i < ( len (f :- p));

      

       A4: (i + 1) <= ( len (f :- p)) by A3, NAT_1: 13;

      

       A5: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

      then (i - 1) < (( len f) - (p .. f)) by A3, XREAL_1: 19;

      then (i -' 1) < (( len f) - (p .. f)) by A2, XREAL_1: 233;

      then ((i -' 1) + (p .. f)) < ( len f) by XREAL_1: 20;

      then

       A6: (((i -' 1) + (p .. f)) + 1) <= ( len f) by NAT_1: 13;

      ((p .. f) - 1) >= 0 by A1, FINSEQ_4: 21, XREAL_1: 48;

      then (( len f) - ((p .. f) - 1)) <= ( len f) by XREAL_1: 43;

      then

       A7: (i + 1) <= ( len f) by A5, A4, XXREAL_0: 2;

      (i -' 1) >= 0 & 1 <= (p .. f) by A1, FINSEQ_4: 21;

      then

       A8: ( 0 + 1) <= ((i -' 1) + (p .. f)) by XREAL_1: 7;

      (((i -' 1) + (p .. f)) + 1) = (((i -' 1) + 1) + (p .. f))

      .= (i + (p .. f)) by A2, XREAL_1: 235

      .= (((i + 1) -' 1) + (p .. f)) by NAT_D: 34;

      then

       A9: (( Rotate (f,p)) /. (i + 1)) = (f /. (((i -' 1) + (p .. f)) + 1)) by A1, A4, Th9, NAT_1: 11;

      

       A10: ( len ( Rotate (f,p))) = ( len f) by Th14;

      (( Rotate (f,p)) /. i) = (f /. ((i -' 1) + (p .. f))) by A1, A2, A3, Th9;

      

      hence ( LSeg (( Rotate (f,p)),i)) = ( LSeg ((f /. ((i -' 1) + (p .. f))),(f /. (((i -' 1) + (p .. f)) + 1)))) by A2, A10, A9, A7, TOPREAL1:def 3

      .= ( LSeg (f,((i -' 1) + (p .. f)))) by A8, A6, TOPREAL1:def 3;

    end;

    theorem :: REVROT_1:25

    

     Th25: p in ( rng f) & (p .. f) <= i & i < ( len f) implies ( LSeg (f,i)) = ( LSeg (( Rotate (f,p)),((i -' (p .. f)) + 1)))

    proof

      assume that

       A1: p in ( rng f) and

       A2: (p .. f) <= i and

       A3: i < ( len f);

      (i - (p .. f)) < (( len f) - (p .. f)) by A3, XREAL_1: 9;

      then (i -' (p .. f)) < (( len f) - (p .. f)) by A2, XREAL_1: 233;

      then ((i -' (p .. f)) + 1) < ((( len f) - (p .. f)) + 1) by XREAL_1: 6;

      then

       A4: ((i -' (p .. f)) + 1) < ( len (f :- p)) by A1, FINSEQ_5: 50;

      (1 + (p .. f)) <= (i + 1) by A2, XREAL_1: 6;

      then 1 <= ((i + 1) -' (p .. f)) by NAT_D: 55;

      then

       A5: 1 <= ((i -' (p .. f)) + 1) by A2, NAT_D: 38;

      ((((i -' (p .. f)) + 1) -' 1) + (p .. f)) = ((i -' (p .. f)) + (p .. f)) by NAT_D: 34

      .= i by A2, XREAL_1: 235;

      hence thesis by A1, A5, A4, Th24;

    end;

    theorem :: REVROT_1:26

    

     Th26: for f be circular FinSequence of ( TOP-REAL 2) holds ( Incr ( X_axis f)) = ( Incr ( X_axis ( Rotate (f,p))))

    proof

      let f be circular FinSequence of ( TOP-REAL 2);

      per cases ;

        suppose not p in ( rng f);

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose p in ( rng f);

        then ( rng ( Rotate (f,p))) = ( rng f) by FINSEQ_6: 90;

        then ( rng ( X_axis ( Rotate (f,p)))) = ( rng ( X_axis f)) by Th21;

        then ( rng ( Incr ( X_axis ( Rotate (f,p))))) = ( rng ( X_axis f)) & ( len ( Incr ( X_axis ( Rotate (f,p))))) = ( card ( rng ( X_axis f))) by SEQ_4:def 21;

        hence thesis by SEQ_4:def 21;

      end;

    end;

    theorem :: REVROT_1:27

    

     Th27: for f be circular FinSequence of ( TOP-REAL 2) holds ( Incr ( Y_axis f)) = ( Incr ( Y_axis ( Rotate (f,p))))

    proof

      let f be circular FinSequence of ( TOP-REAL 2);

      per cases ;

        suppose not p in ( rng f);

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose p in ( rng f);

        then ( rng ( Rotate (f,p))) = ( rng f) by FINSEQ_6: 90;

        then ( rng ( Y_axis ( Rotate (f,p)))) = ( rng ( Y_axis f)) by Th23;

        then ( rng ( Incr ( Y_axis ( Rotate (f,p))))) = ( rng ( Y_axis f)) & ( len ( Incr ( Y_axis ( Rotate (f,p))))) = ( card ( rng ( Y_axis f))) by SEQ_4:def 21;

        hence thesis by SEQ_4:def 21;

      end;

    end;

    theorem :: REVROT_1:28

    

     Th28: for f be non empty circular FinSequence of ( TOP-REAL 2) holds ( GoB ( Rotate (f,p))) = ( GoB f)

    proof

      let f be non empty circular FinSequence of ( TOP-REAL 2);

      ( Incr ( X_axis f)) = ( Incr ( X_axis ( Rotate (f,p)))) & ( Incr ( Y_axis f)) = ( Incr ( Y_axis ( Rotate (f,p)))) by Th26, Th27;

      

      hence ( GoB ( Rotate (f,p))) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2

      .= ( GoB f) by GOBOARD2:def 2;

    end;

    theorem :: REVROT_1:29

    

     Th29: for f be non constant standard special_circular_sequence holds ( Rev ( Rotate (f,p))) = ( Rotate (( Rev f),p))

    proof

      let f be non constant standard special_circular_sequence;

      per cases ;

        suppose not p in ( rng f);

        then ( Rotate (f,p)) = f & not p in ( rng ( Rev f)) by FINSEQ_5: 57, FINSEQ_6:def 2;

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose

         A1: p = (f /. 1);

        

        then

         A2: p = (( Rev f) /. ( len f)) by FINSEQ_5: 65

        .= (( Rev f) /. ( len ( Rev f))) by FINSEQ_5:def 3

        .= (( Rev f) /. 1) by FINSEQ_6:def 1;

        ( Rotate (f,p)) = f by A1, FINSEQ_6: 89;

        hence thesis by A2, FINSEQ_6: 89;

      end;

        suppose that

         A3: p in ( rng f) and

         A4: p <> (f /. 1);

        f just_once_values p

        proof

          take (p .. f);

          thus

           A5: (p .. f) in ( dom f) by A3, FINSEQ_4: 20;

          

          thus

           A6: p = (f . (p .. f)) by A3, FINSEQ_4: 19

          .= (f /. (p .. f)) by A5, PARTFUN1:def 6;

          let z be set such that

           A7: z in ( dom f) and

           A8: z <> (p .. f);

          reconsider k = z as Element of NAT by A7;

          per cases by A8, XXREAL_0: 1;

            suppose

             A9: k < (p .. f);

            (p .. f) <= ( len f) & (p .. f) <> ( len f) by A3, A4, A6, FINSEQ_4: 21, FINSEQ_6:def 1;

            then

             A10: (p .. f) < ( len f) by XXREAL_0: 1;

            1 <= k by A7, FINSEQ_3: 25;

            hence thesis by A6, A9, A10, GOBOARD7: 36;

          end;

            suppose

             A11: k > (p .. f);

            (p .. f) >= 1 by A3, FINSEQ_4: 21;

            then

             A12: (p .. f) > 1 by A4, A6, XXREAL_0: 1;

            k <= ( len f) by A7, FINSEQ_3: 25;

            hence thesis by A6, A11, A12, GOBOARD7: 37;

          end;

        end;

        hence thesis by FINSEQ_6: 106;

      end;

    end;

    begin

    reserve f for circular FinSequence of ( TOP-REAL 2);

    theorem :: REVROT_1:30

    

     Th30: for f be circular s.c.c. FinSequence of ( TOP-REAL 2) st ( len f) > 4 holds (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) = {(f /. 1)}

    proof

      let f be circular s.c.c. FinSequence of ( TOP-REAL 2);

      assume

       A1: ( len f) > 4;

      then

       A2: ((( len f) -' 1) + 1) = ( len f) by XREAL_1: 235, XXREAL_0: 2;

      

       A3: ( len f) >= (1 + 1) by A1, XXREAL_0: 2;

      then

       A4: 1 <= (( len f) -' 1) by NAT_D: 55;

      

       A5: ( len f) >= ((1 + 1) + 1) by A1, XXREAL_0: 2;

      thus (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) c= {(f /. 1)}

      proof

        assume not (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) c= {(f /. 1)};

        then

        consider p be Point of ( TOP-REAL 2) such that

         A6: p in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) and

         A7: not p in {(f /. 1)};

        

         A8: p <> (f /. 1) by A7, TARSKI:def 1;

        

         A9: ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) & ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) by A3, A2, A4, TOPREAL1:def 3;

        

         A10: (f /. ( len f)) = (f /. 1) by FINSEQ_6:def 1;

        per cases by A6, A9, A8, A10, JGRAPH_1: 16;

          suppose

           A11: (f /. (1 + 1)) in ( LSeg (f,(( len f) -' 1)));

          

           A12: (f /. (1 + 1)) in ( LSeg (f,(1 + 1))) by A5, TOPREAL1: 21;

          (3 + 1) = 4;

          then ((1 + 1) + 1) < (( len f) - 1) by A1, XREAL_1: 20;

          then

           A13: ((1 + 1) + 1) < (( len f) -' 1) by A1, XREAL_1: 233, XXREAL_0: 2;

          (( len f) -' 1) < ( len f) by A4, NAT_D: 51;

          then ( LSeg (f,(1 + 1))) misses ( LSeg (f,(( len f) -' 1))) by A13, GOBOARD5:def 4;

          hence contradiction by A11, A12, XBOOLE_0: 3;

        end;

          suppose

           A14: (f /. (( len f) -' 1)) in ( LSeg (f,1));

          

           A15: ((( len f) -' 2) + 1) = (((( len f) -' 1) -' 1) + 1) by NAT_D: 45

          .= (( len f) -' 1) by A3, NAT_D: 55, XREAL_1: 235;

          then

           A16: ((( len f) -' 2) + 1) < ( len f) by A4, NAT_D: 51;

          (2 + 2) < ( len f) by A1;

          then (1 + 1) < (( len f) - 2) by XREAL_1: 20;

          then (1 + 1) < (( len f) -' 2) by A1, XREAL_1: 233, XXREAL_0: 2;

          then

           A17: ( LSeg (f,1)) misses ( LSeg (f,(( len f) -' 2))) by A16, GOBOARD5:def 4;

          1 <= (( len f) - 2) by A5, XREAL_1: 19;

          then 1 <= (( len f) -' 2) by NAT_D: 39;

          then (f /. (( len f) -' 1)) in ( LSeg (f,(( len f) -' 2))) by A15, A16, TOPREAL1: 21;

          hence contradiction by A14, A17, XBOOLE_0: 3;

        end;

      end;

      let x be object;

      assume x in {(f /. 1)};

      then

       A18: x = (f /. 1) by TARSKI:def 1;

      then x = (f /. ( len f)) by FINSEQ_6:def 1;

      then

       A19: x in ( LSeg (f,(( len f) -' 1))) by A2, A4, TOPREAL1: 21;

      x in ( LSeg (f,1)) by A3, A18, TOPREAL1: 21;

      hence thesis by A19, XBOOLE_0:def 4;

    end;

    theorem :: REVROT_1:31

    

     Th31: p in ( rng f) & ( len (f :- p)) <= i & i < ( len f) implies ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i + (p .. f)) -' ( len f))))

    proof

      assume that

       A1: p in ( rng f) and

       A2: ( len (f :- p)) <= i and

       A3: i < ( len f);

      

       A4: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

      

       A5: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

      then ((( len f) -' (p .. f)) + 1) <= i by A2, A4, XREAL_1: 233;

      then ((( len f) + 1) -' (p .. f)) <= i by A4, NAT_D: 38;

      then

       A6: (( len f) + 1) <= (i + (p .. f)) by NAT_D: 52;

      then

       A7: 1 <= ((i + (p .. f)) -' ( len f)) by NAT_D: 55;

      (( len f) - (p .. f)) >= 0 by A4, XREAL_1: 48;

      then ((( len f) - (p .. f)) + 1) >= ( 0 + 1) by XREAL_1: 6;

      then

       A8: ( 0 + 1) <= ( 0 + i) by A2, A5, XXREAL_0: 2;

      

       A9: ( len ( Rotate (f,p))) = ( len f) by Th14;

      

       A10: ( len f) <= (( len f) + 1) by NAT_1: 11;

      

       A11: (i + 1) <= ( len f) by A3, NAT_1: 13;

      then ((i + 1) + (p .. f)) <= (( len f) + ( len f)) by A4, XREAL_1: 7;

      then (((i + (p .. f)) + 1) -' ( len f)) <= ( len f) by NAT_D: 53;

      then

       A12: (((i + (p .. f)) -' ( len f)) + 1) <= ( len f) by A6, A10, NAT_D: 38, XXREAL_0: 2;

      (((i + 1) + (p .. f)) -' ( len f)) = (((i + (p .. f)) + 1) -' ( len f))

      .= (((i + (p .. f)) -' ( len f)) + 1) by A6, A10, NAT_D: 38, XXREAL_0: 2;

      then

       A13: (( Rotate (f,p)) /. (i + 1)) = (f /. (((i + (p .. f)) -' ( len f)) + 1)) by A1, A2, A11, Th17, NAT_1: 12;

      (i + 1) <= ( len f) & (( Rotate (f,p)) /. i) = (f /. ((i + (p .. f)) -' ( len f))) by A1, A2, A3, Th17, NAT_1: 13;

      

      hence ( LSeg (( Rotate (f,p)),i)) = ( LSeg ((f /. ((i + (p .. f)) -' ( len f))),(f /. (((i + (p .. f)) -' ( len f)) + 1)))) by A9, A13, A8, TOPREAL1:def 3

      .= ( LSeg (f,((i + (p .. f)) -' ( len f)))) by A7, A12, TOPREAL1:def 3;

    end;

    registration

      let p be Point of ( TOP-REAL 2);

      let f be circular s.c.c. FinSequence of ( TOP-REAL 2);

      cluster ( Rotate (f,p)) -> s.c.c.;

      coherence

      proof

        set h = ( Rotate (f,p));

        per cases ;

          suppose not p in ( rng f);

          hence thesis by FINSEQ_6:def 2;

        end;

          suppose p in ( rng f) & (p .. f) = 1;

          then p = (f /. 1) by FINSEQ_5: 38;

          hence thesis by FINSEQ_6: 89;

        end;

          suppose p in ( rng f) & (p .. f) = ( len f);

          then p = (f /. ( len f)) by FINSEQ_5: 38;

          then p = (f /. 1) by FINSEQ_6:def 1;

          hence thesis by FINSEQ_6: 89;

        end;

          suppose that

           A1: p in ( rng f) and

           A2: (p .. f) <> 1 and

           A3: (p .. f) <> ( len f);

          

           A4: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

          let i, j such that

           A5: (i + 1) < j and

           A6: i > 1 & j < ( len h) or (j + 1) < ( len h);

          1 <= (p .. f) by A1, FINSEQ_4: 21;

          then (p .. f) > 1 by A2, XXREAL_0: 1;

          then

           A7: ((i -' 1) + (p .. f)) > ( 0 + 1) by XREAL_1: 8;

          i <= (i + 1) by NAT_1: 11;

          then

           A8: i < j by A5, XXREAL_0: 2;

          

           A9: ( len f) = ( len h) by Th14;

          

           A10: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

          then

           A11: (( len f) - (p .. f)) = (( len f) -' (p .. f)) by XREAL_1: 233;

          j <= (j + 1) by NAT_1: 11;

          then

           A12: j < ( len f) by A9, A6, XXREAL_0: 2;

          then

           A13: i < ( len f) by A8, XXREAL_0: 2;

          now

            per cases by NAT_1: 14;

              suppose i = 0 ;

              then ( LSeg (h,i)) = {} by TOPREAL1:def 3;

              hence thesis;

            end;

              suppose that

               A14: i >= 1 and

               A15: j < ( len (f :- p));

              i < ( len (f :- p)) by A8, A15, XXREAL_0: 2;

              then

               A16: ( LSeg (h,i)) = ( LSeg (f,((i -' 1) + (p .. f)))) by A1, A14, Th24;

              

               A17: 1 <= j by A8, A14, XXREAL_0: 2;

              then (j -' 1) < (( len f) -' (p .. f)) by A4, A11, A15, NAT_D: 54;

              then

               A18: ((j -' 1) + (p .. f)) < ( len f) by NAT_D: 53;

              i < (j -' 1) by A5, NAT_D: 52;

              then

               A19: ((i + 1) -' 1) < (j -' 1) by NAT_D: 34;

              (((i -' 1) + (p .. f)) + 1) = (((i -' 1) + 1) + (p .. f))

              .= (i + (p .. f)) by A14, XREAL_1: 235

              .= (((i + 1) -' 1) + (p .. f)) by NAT_D: 34;

              then

               A20: (((i -' 1) + (p .. f)) + 1) < ((j -' 1) + (p .. f)) by A19, XREAL_1: 6;

              ( LSeg (h,j)) = ( LSeg (f,((j -' 1) + (p .. f)))) by A1, A15, A17, Th24;

              hence thesis by A7, A16, A20, A18, GOBOARD5:def 4;

            end;

              suppose that

               A21: i >= 1 and

               A22: j >= ( len (f :- p)) and

               A23: i < ( len (f :- p));

              now

                per cases by A6, Th14;

                  suppose i > 1;

                  then i >= (1 + 1) by NAT_1: 13;

                  then (i -' 1) >= 1 by NAT_D: 55;

                  hence (j + 1) < ((i -' 1) + ( len f)) by A12, XREAL_1: 8;

                end;

                  suppose

                   A24: (j + 1) < ( len f);

                  ( 0 + ( len f)) <= ((i -' 1) + ( len f)) by XREAL_1: 6;

                  hence (j + 1) < ((i -' 1) + ( len f)) by A24, XXREAL_0: 2;

                end;

              end;

              then ((j + 1) + (p .. f)) < (((i -' 1) + ( len f)) + (p .. f)) by XREAL_1: 6;

              then

               A25: ((j + (p .. f)) + 1) < (((i -' 1) + (p .. f)) + ( len f));

              (( len f) -' (p .. f)) <= ((( len f) -' (p .. f)) + 1) by NAT_1: 11;

              then (( len f) - (p .. f)) <= j by A4, A11, A22, XXREAL_0: 2;

              then

               A26: ( len f) <= (j + (p .. f)) by XREAL_1: 20;

              then ( len f) <= ((j + (p .. f)) + 1) by NAT_1: 12;

              then (((j + (p .. f)) + 1) -' ( len f)) < ((i -' 1) + (p .. f)) by A25, NAT_D: 54;

              then

               A27: (((j + (p .. f)) -' ( len f)) + 1) < ((i -' 1) + (p .. f)) by A26, NAT_D: 38;

              

               A28: ( LSeg (h,i)) = ( LSeg (f,((i -' 1) + (p .. f)))) & ( LSeg (h,j)) = ( LSeg (f,((j + (p .. f)) -' ( len f)))) by A1, A12, A21, A22, A23, Th24, Th31;

              now

                per cases by A5, XXREAL_0: 2;

                  suppose j > ((( len f) - (p .. f)) + 1);

                  then 1 < (j - (( len f) - (p .. f))) by XREAL_1: 20;

                  then 1 < ((j + (p .. f)) - ( len f));

                  then

                   A29: 1 < ((j + (p .. f)) -' ( len f)) by NAT_D: 39;

                  i < ((( len f) -' (p .. f)) + 1) by A4, A10, A23, XREAL_1: 233;

                  then (i -' 1) < (( len f) -' (p .. f)) by A21, NAT_D: 54;

                  then ((i -' 1) + (p .. f)) < ( len f) by NAT_D: 53;

                  hence thesis by A28, A27, A29, GOBOARD5:def 4;

                end;

                  suppose (i + 1) < ((( len f) - (p .. f)) + 1);

                  then i < (( len f) - (p .. f)) by XREAL_1: 6;

                  then (i + (p .. f)) < ( len f) by XREAL_1: 20;

                  then (((i -' 1) + 1) + (p .. f)) < ( len f) by A21, XREAL_1: 235;

                  then (((i -' 1) + (p .. f)) + 1) < ( len f);

                  hence thesis by A28, A27, GOBOARD5:def 4;

                end;

              end;

              hence thesis;

            end;

              suppose

               A30: i >= ( len (f :- p));

              then j >= ( len (f :- p)) by A8, XXREAL_0: 2;

              then

               A31: ( LSeg (h,j)) = ( LSeg (f,((j + (p .. f)) -' ( len f)))) by A1, A12, Th31;

              (( len f) - (p .. f)) <= ((( len f) - (p .. f)) + 1) by XREAL_1: 29;

              then

               A32: (( len f) - (p .. f)) <= i by A4, A30, XXREAL_0: 2;

              then

               A33: ( len f) <= (i + (p .. f)) by A11, NAT_D: 52;

              

               A34: (i + (p .. f)) < (j + (p .. f)) by A8, XREAL_1: 6;

              then

               A35: ( len f) < (j + (p .. f)) by A33, XXREAL_0: 2;

              (j + 1) <= ( len f) & (p .. f) < ( len f) by A3, A10, A9, A6, NAT_1: 13, XXREAL_0: 1;

              then ((j + 1) + (p .. f)) < (( len f) + ( len f)) by XREAL_1: 8;

              then ((j + (1 + (p .. f))) - ( len f)) < ( len f) by XREAL_1: 19;

              then (((j + (p .. f)) - ( len f)) + 1) < ( len f);

              then

               A36: (((j + (p .. f)) -' ( len f)) + 1) < ( len f) by A33, A34, XREAL_1: 233, XXREAL_0: 2;

              

               A37: ((i + 1) + (p .. f)) < (j + (p .. f)) by A5, XREAL_1: 6;

              (((i + (p .. f)) -' ( len f)) + 1) = (((i + (p .. f)) + 1) -' ( len f)) by A11, A32, NAT_D: 38, NAT_D: 52

              .= (((i + 1) + (p .. f)) -' ( len f));

              then

               A38: (((i + (p .. f)) -' ( len f)) + 1) < ((j + (p .. f)) -' ( len f)) by A35, A37, NAT_D: 57;

              ( LSeg (h,i)) = ( LSeg (f,((i + (p .. f)) -' ( len f)))) by A1, A13, A30, Th31;

              hence thesis by A31, A38, A36, GOBOARD5:def 4;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    registration

      let p be Point of ( TOP-REAL 2);

      let f be non constant standard special_circular_sequence;

      cluster ( Rotate (f,p)) -> unfolded;

      coherence

      proof

        per cases ;

          suppose not p in ( rng f);

          hence thesis by FINSEQ_6:def 2;

        end;

          suppose

           A1: p in ( rng f);

          let i be Nat such that

           A2: 1 <= i and

           A3: (i + 2) <= ( len ( Rotate (f,p)));

          

           A4: ( len f) > 4 by GOBOARD7: 34;

          thus (( LSeg (( Rotate (f,p)),i)) /\ ( LSeg (( Rotate (f,p)),(i + 1)))) = {(( Rotate (f,p)) /. (i + 1))}

          proof

            

             A5: (((i + 1) -' 1) + (p .. f)) = (i + (p .. f)) by NAT_D: 34

            .= (((i -' 1) + 1) + (p .. f)) by A2, XREAL_1: 235

            .= (((i -' 1) + (p .. f)) + 1);

            

             A6: ( len f) = ( len ( Rotate (f,p))) by Th14;

            (i + 1) < (i + 2) by XREAL_1: 6;

            then

             A7: (i + 1) < ( len f) by A3, A6, XXREAL_0: 2;

            

             A8: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

            per cases by XXREAL_0: 1;

              suppose

               A9: (i + 1) = ( len (f :- p));

              ((( len (f :- p)) + (p .. f)) -' ( len f)) = ((( len f) + 1) - ( len f)) by A8, NAT_1: 11, XREAL_1: 233

              .= 1;

              then

               A10: ( LSeg (( Rotate (f,p)),( len (f :- p)))) = ( LSeg (f,1)) by A1, A7, A9, Th31;

              

               A11: i < ( len (f :- p)) by A9, XREAL_1: 29;

              ((i -' 1) + (p .. f)) = (((((( len f) - (p .. f)) + 1) - 1) - 1) + (p .. f)) by A2, A8, A9, XREAL_1: 233

              .= (((( len f) - (p .. f)) + (p .. f)) - 1)

              .= (( len f) -' 1) by A4, XREAL_1: 233, XXREAL_0: 2;

              then ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,(( len f) -' 1))) by A1, A2, A11, Th24;

              

              hence (( LSeg (( Rotate (f,p)),i)) /\ ( LSeg (( Rotate (f,p)),(i + 1)))) = {(f /. 1)} by A9, A10, Th30, GOBOARD7: 34

              .= {(f /. ( len f))} by FINSEQ_6:def 1

              .= {(( Rotate (f,p)) /. (i + 1))} by A1, A9, Th11;

            end;

              suppose

               A12: (i + 1) < ( len (f :- p));

              then (i + 1) < ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

              then i < (( len f) - (p .. f)) by XREAL_1: 6;

              then (i + (p .. f)) < ( len f) by XREAL_1: 20;

              then (((i -' 1) + 1) + (p .. f)) < ( len f) by A2, XREAL_1: 235;

              then ((((i -' 1) + (p .. f)) + 1) + 1) <= ( len f) by NAT_1: 13;

              then

               A13: (((i -' 1) + (p .. f)) + (1 + 1)) <= ( len f);

              ((i -' 1) + (p .. f)) >= (p .. f) & (p .. f) >= 1 by A1, FINSEQ_4: 21, NAT_1: 11;

              then

               A14: 1 <= ((i -' 1) + (p .. f)) by XXREAL_0: 2;

              (i + 0 ) < (i + 1) by XREAL_1: 6;

              then i < ( len (f :- p)) by A12, XXREAL_0: 2;

              then

               A15: ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i -' 1) + (p .. f)))) by A1, A2, Th24;

              ( LSeg (( Rotate (f,p)),(i + 1))) = ( LSeg (f,(((i + 1) -' 1) + (p .. f)))) by A1, A12, Th24, NAT_1: 11;

              

              hence (( LSeg (( Rotate (f,p)),i)) /\ ( LSeg (( Rotate (f,p)),(i + 1)))) = {(f /. (((i + 1) -' 1) + (p .. f)))} by A5, A15, A14, A13, TOPREAL1:def 6

              .= {(( Rotate (f,p)) /. (i + 1))} by A1, A12, Th9, NAT_1: 11;

            end;

              suppose

               A16: ( len (f :- p)) < (i + 1);

              (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

              then ((i + 2) + (p .. f)) <= (( len f) + ( len f)) by A3, A6, XREAL_1: 7;

              then (((i + (p .. f)) + 2) - ( len f)) <= ( len f) by XREAL_1: 20;

              then

               A17: (((i + (p .. f)) - ( len f)) + 2) <= ( len f);

              ((i + 1) + 1) <= ( len f) by A3, Th14;

              then

               A18: (i + 1) < ( len f) by NAT_1: 13;

              (i + 1) > ((( len f) - (p .. f)) + 1) by A1, A16, FINSEQ_5: 50;

              then (( len f) - (p .. f)) < i by XREAL_1: 6;

              then

               A19: ( len f) < (i + (p .. f)) by XREAL_1: 19;

              then

               A20: ((i + (p .. f)) -' ( len f)) = ((i + (p .. f)) - ( len f)) by XREAL_1: 233;

               0 < ((i + (p .. f)) - ( len f)) by A19, XREAL_1: 50;

              then

               A21: ( 0 + 1) <= ((i + (p .. f)) -' ( len f)) by A20, NAT_1: 13;

              

               A22: (((i + 1) + (p .. f)) -' ( len f)) = (((i + (p .. f)) + 1) -' ( len f))

              .= (((i + (p .. f)) -' ( len f)) + 1) by A19, NAT_D: 38;

              

               A23: ( len (f :- p)) <= i by A16, NAT_1: 13;

              (i + 0 ) < (i + 1) by XREAL_1: 6;

              then i < ( len f) by A18, XXREAL_0: 2;

              then

               A24: ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i + (p .. f)) -' ( len f)))) by A1, A23, Th31;

              ( LSeg (( Rotate (f,p)),(i + 1))) = ( LSeg (f,(((i + 1) + (p .. f)) -' ( len f)))) by A1, A16, A18, Th31;

              

              hence (( LSeg (( Rotate (f,p)),i)) /\ ( LSeg (( Rotate (f,p)),(i + 1)))) = {(f /. (((i + 1) + (p .. f)) -' ( len f)))} by A24, A20, A21, A22, A17, TOPREAL1:def 6

              .= {(( Rotate (f,p)) /. (i + 1))} by A1, A7, A16, Th17;

            end;

          end;

        end;

      end;

    end

    theorem :: REVROT_1:32

    

     Th32: p in ( rng f) & 1 <= i & i < (p .. f) implies ( LSeg (f,i)) = ( LSeg (( Rotate (f,p)),((i + ( len f)) -' (p .. f))))

    proof

      assume that

       A1: p in ( rng f) and

       A2: 1 <= i and

       A3: i < (p .. f);

      

       A4: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

      

       A5: (i + ( len f)) < (( len f) + (p .. f)) by A3, XREAL_1: 6;

      

       A6: ( len f) <= (i + ( len f)) by NAT_1: 11;

      then (p .. f) <= (i + ( len f)) by A4, XXREAL_0: 2;

      then

       A7: ((i + ( len f)) -' (p .. f)) < ( len f) by A5, NAT_D: 54;

      (( len f) + 1) <= (i + ( len f)) by A2, XREAL_1: 6;

      then ((( len f) + 1) -' (p .. f)) <= ((i + ( len f)) -' (p .. f)) by NAT_D: 42;

      then ((( len f) -' (p .. f)) + 1) <= ((i + ( len f)) -' (p .. f)) by A4, NAT_D: 38;

      then ((( len f) - (p .. f)) + 1) <= ((i + ( len f)) -' (p .. f)) by A4, XREAL_1: 233;

      then

       A8: ( len (f :- p)) <= ((i + ( len f)) -' (p .. f)) by A1, FINSEQ_5: 50;

      ((((i + ( len f)) -' (p .. f)) + (p .. f)) -' ( len f)) = ((i + ( len f)) -' ( len f)) by A4, A6, XREAL_1: 235, XXREAL_0: 2

      .= i by NAT_D: 34;

      hence thesis by A1, A8, A7, Th31;

    end;

    theorem :: REVROT_1:33

    

     Th33: ( L~ ( Rotate (f,p))) = ( L~ f)

    proof

      per cases ;

        suppose not p in ( rng f);

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose

         A1: p in ( rng f);

        set B = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

        set A = { ( LSeg (( Rotate (f,p)),i)) : 1 <= i & (i + 1) <= ( len f) };

        

         A2: A = B

        proof

          

           A3: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

          thus A c= B

          proof

            

             A4: 1 <= (p .. f) by A1, FINSEQ_4: 21;

            let x be object;

            assume x in A;

            then

            consider i such that

             A5: x = ( LSeg (( Rotate (f,p)),i)) and

             A6: 1 <= i and

             A7: (i + 1) <= ( len f);

            

             A8: i < ( len f) by A7, NAT_1: 13;

            per cases ;

              suppose

               A9: i < ( len (f :- p));

              then i < ((( len f) - (p .. f)) + 1) by A1, FINSEQ_5: 50;

              then i < ((( len f) -' (p .. f)) + 1) by A3, XREAL_1: 233;

              then (i -' 1) < (( len f) -' (p .. f)) by A6, NAT_D: 54;

              then ((i -' 1) + (p .. f)) < ( len f) by NAT_D: 53;

              then

               A10: (((i -' 1) + (p .. f)) + 1) <= ( len f) by NAT_1: 13;

              (1 + 1) <= (i + (p .. f)) by A6, A4, XREAL_1: 7;

              then 1 <= ((i + (p .. f)) -' 1) by NAT_D: 55;

              then

               A11: 1 <= ((i -' 1) + (p .. f)) by A6, NAT_D: 38;

              ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i -' 1) + (p .. f)))) by A1, A6, A9, Th24;

              hence thesis by A5, A11, A10;

            end;

              suppose

               A12: i >= ( len (f :- p));

              then ((( len f) - (p .. f)) + 1) <= i by A1, FINSEQ_5: 50;

              then ((( len f) -' (p .. f)) + 1) <= i by A3, XREAL_1: 233;

              then ((1 + ( len f)) -' (p .. f)) <= i by A3, NAT_D: 38;

              then

               A13: (1 + ( len f)) <= (i + (p .. f)) by NAT_D: 52;

              then

               A14: 1 <= ((i + (p .. f)) -' ( len f)) by NAT_D: 55;

              ((i + 1) + (p .. f)) <= (( len f) + ( len f)) by A3, A7, XREAL_1: 7;

              then ( len f) <= (( len f) + 1) & (((i + (p .. f)) + 1) -' ( len f)) <= ( len f) by NAT_1: 11, NAT_D: 53;

              then

               A15: (((i + (p .. f)) -' ( len f)) + 1) <= ( len f) by A13, NAT_D: 38, XXREAL_0: 2;

              ( LSeg (( Rotate (f,p)),i)) = ( LSeg (f,((i + (p .. f)) -' ( len f)))) by A1, A8, A12, Th31;

              hence thesis by A5, A14, A15;

            end;

          end;

          let x be object;

          assume x in B;

          then

          consider i such that

           A16: x = ( LSeg (f,i)) and

           A17: 1 <= i and

           A18: (i + 1) <= ( len f);

          

           A19: i < ( len f) by A18, NAT_1: 13;

          per cases ;

            suppose

             A20: (p .. f) <= i;

            i <= (i + 1) by NAT_1: 11;

            then

             A21: (p .. f) <= (i + 1) by A20, XXREAL_0: 2;

            1 <= (p .. f) by A1, FINSEQ_4: 21;

            then (i + 1) < (( len f) + (p .. f)) by A19, XREAL_1: 8;

            then ((i + 1) -' (p .. f)) < ( len f) by A21, NAT_D: 54;

            then ((i -' (p .. f)) + 1) < ( len f) by A20, NAT_D: 38;

            then

             A22: (((i -' (p .. f)) + 1) + 1) <= ( len f) by NAT_1: 13;

            (1 + (p .. f)) <= (i + 1) by A20, XREAL_1: 6;

            then 1 <= ((i + 1) -' (p .. f)) by NAT_D: 55;

            then

             A23: 1 <= ((i -' (p .. f)) + 1) by A20, NAT_D: 38;

            ( LSeg (f,i)) = ( LSeg (( Rotate (f,p)),((i -' (p .. f)) + 1))) by A1, A19, A20, Th25;

            hence thesis by A16, A23, A22;

          end;

            suppose

             A24: i < (p .. f);

            then (i + 1) <= (p .. f) by NAT_1: 13;

            then ((i + 1) + ( len f)) <= (( len f) + (p .. f)) by XREAL_1: 6;

            then

             A25: (((i + ( len f)) + 1) -' (p .. f)) <= ( len f) by NAT_D: 53;

            (p .. f) <= ( len f) & ( len f) <= (i + ( len f)) by A1, FINSEQ_4: 21, NAT_1: 11;

            then

             A26: (((i + ( len f)) -' (p .. f)) + 1) <= ( len f) by A25, NAT_D: 38, XXREAL_0: 2;

            (1 + (p .. f)) <= (i + ( len f)) by A3, A17, XREAL_1: 7;

            then

             A27: 1 <= ((i + ( len f)) -' (p .. f)) by NAT_D: 55;

            ( LSeg (f,i)) = ( LSeg (( Rotate (f,p)),((i + ( len f)) -' (p .. f)))) by A1, A17, A24, Th32;

            hence thesis by A16, A27, A26;

          end;

        end;

        ( len ( Rotate (f,p))) = ( len f) by Th14;

        hence thesis by A2;

      end;

    end;

    theorem :: REVROT_1:34

    

     Th34: for G be Go-board holds f is_sequence_on G iff ( Rotate (f,p)) is_sequence_on G

    proof

      let G be Go-board;

      

       A1: ( dom f) = ( dom ( Rotate (f,p))) by Th15;

      

       A2: ( len f) = ( len ( Rotate (f,p))) by Th14;

      per cases ;

        suppose not p in ( rng f);

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose

         A3: p in ( rng f);

        then

         A4: (p .. f) <= ( len f) by FINSEQ_4: 21;

        

         A5: 1 <= (p .. f) by A3, FINSEQ_4: 21;

        thus f is_sequence_on G implies ( Rotate (f,p)) is_sequence_on G

        proof

          assume

           A6: f is_sequence_on G;

          thus for n st n in ( dom ( Rotate (f,p))) holds ex i, j st [i, j] in ( Indices G) & (( Rotate (f,p)) /. n) = (G * (i,j))

          proof

            let n;

            assume

             A7: n in ( dom ( Rotate (f,p)));

            then

             A8: 1 <= n by FINSEQ_3: 25;

            

             A9: n <= ( len ( Rotate (f,p))) by A7, FINSEQ_3: 25;

            per cases ;

              suppose

               A10: ( len (f :- p)) <= n;

              then ((( len f) - (p .. f)) + 1) <= n by A3, FINSEQ_5: 50;

              then ((( len f) -' (p .. f)) + 1) <= n by A4, XREAL_1: 233;

              then ((( len f) + 1) -' (p .. f)) <= n by A4, NAT_D: 38;

              then (( len f) + 1) <= (n + (p .. f)) by NAT_D: 52;

              then

               A11: 1 <= ((n + (p .. f)) -' ( len f)) by NAT_D: 55;

              (n + (p .. f)) <= (( len f) + ( len f)) by A2, A4, A9, XREAL_1: 7;

              then ((n + (p .. f)) -' ( len f)) <= ( len f) by NAT_D: 53;

              then ((n + (p .. f)) -' ( len f)) in ( dom ( Rotate (f,p))) by A2, A11, FINSEQ_3: 25;

              then

              consider i, j such that

               A12: [i, j] in ( Indices G) and

               A13: (f /. ((n + (p .. f)) -' ( len f))) = (G * (i,j)) by A1, A6;

              take i, j;

              thus [i, j] in ( Indices G) by A12;

              thus thesis by A2, A3, A9, A10, A13, Th17;

            end;

              suppose

               A14: ( len (f :- p)) >= n;

              then ((( len f) - (p .. f)) + 1) >= n by A3, FINSEQ_5: 50;

              then ((( len f) -' (p .. f)) + 1) >= n by A4, XREAL_1: 233;

              then (n -' 1) <= (( len f) -' (p .. f)) by NAT_D: 53;

              then

               A15: ((n -' 1) + (p .. f)) <= ( len f) by A4, NAT_D: 54;

              (1 + 1) <= (n + (p .. f)) by A5, A8, XREAL_1: 7;

              then 1 <= ((n + (p .. f)) -' 1) by NAT_D: 55;

              then 1 <= ((n -' 1) + (p .. f)) by A8, NAT_D: 38;

              then ((n -' 1) + (p .. f)) in ( dom ( Rotate (f,p))) by A2, A15, FINSEQ_3: 25;

              then

              consider i, j such that

               A16: [i, j] in ( Indices G) and

               A17: (f /. ((n -' 1) + (p .. f))) = (G * (i,j)) by A1, A6;

              take i, j;

              thus [i, j] in ( Indices G) by A16;

              thus thesis by A3, A8, A14, A17, Th9;

            end;

          end;

          let n such that

           A18: n in ( dom ( Rotate (f,p))) and

           A19: (n + 1) in ( dom ( Rotate (f,p)));

          

           A20: 1 <= n by A18, FINSEQ_3: 25;

          

           A21: n <= ( len f) by A1, A18, FINSEQ_3: 25;

          

           A22: 1 <= (n + 1) by A19, FINSEQ_3: 25;

          

           A23: (n + 1) <= ( len f) by A1, A19, FINSEQ_3: 25;

          let m, k, i, j such that

           A24: [m, k] in ( Indices G) & [i, j] in ( Indices G) & (( Rotate (f,p)) /. n) = (G * (m,k)) & (( Rotate (f,p)) /. (n + 1)) = (G * (i,j));

          thus ( |.(m - i).| + |.(k - j).|) = 1

          proof

            per cases ;

              suppose that

               A25: ( len (f :- p)) <= n;

              ((( len f) - (p .. f)) + 1) <= n by A3, A25, FINSEQ_5: 50;

              then ((( len f) -' (p .. f)) + 1) <= n by A4, XREAL_1: 233;

              then ((( len f) + 1) -' (p .. f)) <= n by A4, NAT_D: 38;

              then (( len f) + 1) <= (n + (p .. f)) by NAT_D: 52;

              then

               A26: 1 <= ((n + (p .. f)) -' ( len f)) by NAT_D: 55;

              (n + (p .. f)) <= (( len f) + ( len f)) by A4, A21, XREAL_1: 7;

              then ((n + (p .. f)) -' ( len f)) <= ( len f) by NAT_D: 53;

              then

               A27: ((n + (p .. f)) -' ( len f)) in ( dom f) by A26, FINSEQ_3: 25;

              n <= (n + 1) by NAT_1: 11;

              then

               A28: ( len (f :- p)) <= (n + 1) by A25, XXREAL_0: 2;

              then

               A29: ((( len f) - (p .. f)) + 1) <= (n + 1) by A3, FINSEQ_5: 50;

              then (( len f) - (p .. f)) <= n by XREAL_1: 6;

              then

               A30: ( len f) <= (n + (p .. f)) by XREAL_1: 20;

              

               A31: (( Rotate (f,p)) /. (n + 1)) = (f /. (((n + 1) + (p .. f)) -' ( len f))) by A3, A23, A28, Th17;

              

               A32: (((n + 1) + (p .. f)) -' ( len f)) = (((n + (p .. f)) + 1) -' ( len f))

              .= (((n + (p .. f)) -' ( len f)) + 1) by A30, NAT_D: 38;

              ((( len f) -' (p .. f)) + 1) <= (n + 1) by A4, A29, XREAL_1: 233;

              then ((( len f) + 1) -' (p .. f)) <= (n + 1) by A4, NAT_D: 38;

              then (( len f) + 1) <= ((n + 1) + (p .. f)) by NAT_D: 52;

              then

               A33: 1 <= (((n + 1) + (p .. f)) -' ( len f)) by NAT_D: 55;

              ((n + 1) + (p .. f)) <= (( len f) + ( len f)) by A4, A23, XREAL_1: 7;

              then (((n + 1) + (p .. f)) -' ( len f)) <= ( len f) by NAT_D: 53;

              then

               A34: (((n + 1) + (p .. f)) -' ( len f)) in ( dom f) by A33, FINSEQ_3: 25;

              (( Rotate (f,p)) /. n) = (f /. ((n + (p .. f)) -' ( len f))) by A3, A21, A25, Th17;

              hence thesis by A6, A24, A31, A32, A27, A34;

            end;

              suppose

               A35: ( len (f :- p)) > n;

              then n <= ((( len f) - (p .. f)) + 1) by A3, FINSEQ_5: 50;

              then n <= ((( len f) -' (p .. f)) + 1) by A4, XREAL_1: 233;

              then (n -' 1) <= (( len f) -' (p .. f)) by NAT_D: 53;

              then

               A36: ((n -' 1) + (p .. f)) <= ( len f) by A4, NAT_D: 54;

              (1 + 1) <= (n + (p .. f)) by A5, A20, XREAL_1: 7;

              then 1 <= ((n + (p .. f)) -' 1) by NAT_D: 55;

              then 1 <= ((n -' 1) + (p .. f)) by A20, NAT_D: 38;

              then

               A37: ((n -' 1) + (p .. f)) in ( dom f) by A36, FINSEQ_3: 25;

              

               A38: (((n + 1) -' 1) + (p .. f)) = (n + (p .. f)) by NAT_D: 34

              .= (((n -' 1) + 1) + (p .. f)) by A20, XREAL_1: 235

              .= (((n -' 1) + (p .. f)) + 1);

              

               A39: ( len (f :- p)) >= (n + 1) by A35, NAT_1: 13;

              then

               A40: (( Rotate (f,p)) /. (n + 1)) = (f /. (((n + 1) -' 1) + (p .. f))) by A3, A22, Th9;

              (n + 1) <= ((( len f) - (p .. f)) + 1) by A3, A39, FINSEQ_5: 50;

              then (n + 1) <= ((( len f) -' (p .. f)) + 1) by A4, XREAL_1: 233;

              then ((n + 1) -' 1) <= (( len f) -' (p .. f)) by NAT_D: 53;

              then

               A41: (((n + 1) -' 1) + (p .. f)) <= ( len f) by A4, NAT_D: 54;

              (1 + 1) <= ((n + 1) + (p .. f)) by A5, A22, XREAL_1: 7;

              then 1 <= (((n + 1) + (p .. f)) -' 1) by NAT_D: 55;

              then 1 <= (((n + 1) -' 1) + (p .. f)) by A22, NAT_D: 38;

              then

               A42: (((n + 1) -' 1) + (p .. f)) in ( dom f) by A41, FINSEQ_3: 25;

              (( Rotate (f,p)) /. n) = (f /. ((n -' 1) + (p .. f))) by A3, A20, A35, Th9;

              hence thesis by A6, A24, A40, A38, A37, A42;

            end;

          end;

        end;

        assume

         A43: ( Rotate (f,p)) is_sequence_on G;

        thus for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))

        proof

          let n;

          assume

           A44: n in ( dom f);

          then

           A45: 1 <= n by FINSEQ_3: 25;

          

           A46: n <= ( len f) by A44, FINSEQ_3: 25;

          per cases ;

            suppose

             A47: n <= (p .. f);

            n <= (n + (( len f) -' (p .. f))) by NAT_1: 11;

            then 1 <= (n + (( len f) -' (p .. f))) by A45, XXREAL_0: 2;

            then

             A48: 1 <= ((n + ( len f)) -' (p .. f)) by A4, NAT_D: 38;

            (n + ( len f)) <= (( len f) + (p .. f)) by A47, XREAL_1: 6;

            then ((n + ( len f)) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then ((n + ( len f)) -' (p .. f)) in ( dom f) by A48, FINSEQ_3: 25;

            then

            consider i, j such that

             A49: [i, j] in ( Indices G) and

             A50: (( Rotate (f,p)) /. ((n + ( len f)) -' (p .. f))) = (G * (i,j)) by A1, A43;

            take i, j;

            thus [i, j] in ( Indices G) by A49;

            thus thesis by A3, A45, A47, A50, Th18;

          end;

            suppose

             A51: n >= (p .. f);

            then (1 + (p .. f)) <= (n + 1) by XREAL_1: 6;

            then

             A52: 1 <= ((n + 1) -' (p .. f)) by NAT_D: 55;

            (n + 1) <= (( len f) + (p .. f)) by A5, A46, XREAL_1: 7;

            then ((n + 1) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then ((n + 1) -' (p .. f)) in ( dom f) by A52, FINSEQ_3: 25;

            then

            consider i, j such that

             A53: [i, j] in ( Indices G) and

             A54: (( Rotate (f,p)) /. ((n + 1) -' (p .. f))) = (G * (i,j)) by A1, A43;

            take i, j;

            thus [i, j] in ( Indices G) by A53;

            thus thesis by A3, A46, A51, A54, Th10;

          end;

        end;

        let n such that

         A55: n in ( dom f) and

         A56: (n + 1) in ( dom f);

        

         A57: 1 <= n by A55, FINSEQ_3: 25;

        

         A58: 1 <= (n + 1) by A56, FINSEQ_3: 25;

        

         A59: n <= ( len f) by A55, FINSEQ_3: 25;

        

         A60: (n + 1) <= ( len f) by A56, FINSEQ_3: 25;

        let m, k, i, j such that

         A61: [m, k] in ( Indices G) & [i, j] in ( Indices G) & (f /. n) = (G * (m,k)) & (f /. (n + 1)) = (G * (i,j));

        thus ( |.(m - i).| + |.(k - j).|) = 1

        proof

          per cases ;

            suppose

             A62: n < (p .. f);

            n <= (n + (( len f) -' (p .. f))) by NAT_1: 11;

            then 1 <= (n + (( len f) -' (p .. f))) by A57, XXREAL_0: 2;

            then

             A63: 1 <= ((n + ( len f)) -' (p .. f)) by A4, NAT_D: 38;

            (n + ( len f)) <= (( len f) + (p .. f)) by A62, XREAL_1: 6;

            then ((n + ( len f)) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then

             A64: ((n + ( len f)) -' (p .. f)) in ( dom f) by A63, FINSEQ_3: 25;

            

             A65: (((n + 1) + ( len f)) -' (p .. f)) = ((( len f) -' (p .. f)) + (n + 1)) by A4, NAT_D: 38

            .= (((( len f) -' (p .. f)) + n) + 1)

            .= (((n + ( len f)) -' (p .. f)) + 1) by A4, NAT_D: 38;

            (n + 1) <= ((n + 1) + (( len f) -' (p .. f))) by NAT_1: 11;

            then 1 <= ((n + 1) + (( len f) -' (p .. f))) by A58, XXREAL_0: 2;

            then

             A66: 1 <= (((n + 1) + ( len f)) -' (p .. f)) by A4, NAT_D: 38;

            

             A67: (n + 1) <= (p .. f) by A62, NAT_1: 13;

            then

             A68: (f /. (n + 1)) = (( Rotate (f,p)) /. (((n + 1) + ( len f)) -' (p .. f))) by A3, A58, Th18;

            ((n + 1) + ( len f)) <= (( len f) + (p .. f)) by A67, XREAL_1: 6;

            then (((n + 1) + ( len f)) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then

             A69: (((n + 1) + ( len f)) -' (p .. f)) in ( dom f) by A66, FINSEQ_3: 25;

            (f /. n) = (( Rotate (f,p)) /. ((n + ( len f)) -' (p .. f))) by A3, A57, A62, Th18;

            hence thesis by A1, A43, A61, A68, A65, A64, A69;

          end;

            suppose

             A70: n >= (p .. f);

            then (1 + (p .. f)) <= (n + 1) by XREAL_1: 6;

            then

             A71: 1 <= ((n + 1) -' (p .. f)) by NAT_D: 55;

            (n + 1) <= (( len f) + (p .. f)) by A5, A59, XREAL_1: 7;

            then ((n + 1) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then

             A72: ((n + 1) -' (p .. f)) in ( dom f) by A71, FINSEQ_3: 25;

            

             A73: (f /. n) = (( Rotate (f,p)) /. ((n + 1) -' (p .. f))) by A3, A59, A70, Th10;

            

             A74: n <= (n + 1) by NAT_1: 11;

            then

             A75: (((n + 1) + 1) -' (p .. f)) = (((n + 1) -' (p .. f)) + 1) by A70, NAT_D: 38, XXREAL_0: 2;

            

             A76: (n + 1) >= (p .. f) by A70, A74, XXREAL_0: 2;

            then (1 + (p .. f)) <= ((n + 1) + 1) by XREAL_1: 6;

            then

             A77: 1 <= (((n + 1) + 1) -' (p .. f)) by NAT_D: 55;

            ((n + 1) + 1) <= (( len f) + (p .. f)) by A5, A60, XREAL_1: 7;

            then (((n + 1) + 1) -' (p .. f)) <= ( len f) by NAT_D: 53;

            then

             A78: (((n + 1) + 1) -' (p .. f)) in ( dom f) by A77, FINSEQ_3: 25;

            (f /. (n + 1)) = (( Rotate (f,p)) /. (((n + 1) + 1) -' (p .. f))) by A3, A60, A76, Th10;

            hence thesis by A1, A43, A61, A73, A75, A78, A72;

          end;

        end;

      end;

    end;

    registration

      let p be Point of ( TOP-REAL 2);

      let f be standard non empty circular FinSequence of ( TOP-REAL 2);

      cluster ( Rotate (f,p)) -> standard;

      coherence

      proof

        ( GoB ( Rotate (f,p))) = ( GoB f) & f is_sequence_on ( GoB f) by Th28, GOBOARD5:def 5;

        hence ( Rotate (f,p)) is_sequence_on ( GoB ( Rotate (f,p))) by Th34;

      end;

    end

    theorem :: REVROT_1:35

    

     Th35: for f be non constant standard special_circular_sequence, p, k st p in ( rng f) & 1 <= k & k < (p .. f) holds ( left_cell (f,k)) = ( left_cell (( Rotate (f,p)),((k + ( len f)) -' (p .. f))))

    proof

      let f be non constant standard special_circular_sequence, p, k such that

       A1: p in ( rng f) and

       A2: 1 <= k and

       A3: k < (p .. f);

      set n = ((k + ( len f)) -' (p .. f));

      

       A4: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

      then k < ( len f) by A3, XXREAL_0: 2;

      then

       A5: (k + 1) <= ( len f) by NAT_1: 13;

       0 < k by A2;

      then

       A6: ( 0 + 1) < (k + 1) by XREAL_1: 6;

      ( len f) <= (k + ( len f)) by NAT_1: 11;

      then

       A7: (n + 1) = (((k + ( len f)) + 1) -' (p .. f)) by A4, NAT_D: 38, XXREAL_0: 2;

      

       A8: (k + 1) <= (p .. f) by A3, NAT_1: 13;

      then ((k + 1) + ( len f)) <= (( len f) + (p .. f)) by XREAL_1: 6;

      then (n + 1) <= ( len f) by A7, NAT_D: 53;

      then

       A9: (n + 1) <= ( len ( Rotate (f,p))) by Th14;

      

       A10: (n + 1) = (((k + 1) + ( len f)) -' (p .. f)) by A7;

      

       A11: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB ( Rotate (f,p)))) & [i2, j2] in ( Indices ( GoB ( Rotate (f,p)))) & (( Rotate (f,p)) /. n) = (( GoB ( Rotate (f,p))) * (i1,j1)) & (( Rotate (f,p)) /. (n + 1)) = (( GoB ( Rotate (f,p))) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k)) = ( cell (( GoB ( Rotate (f,p))),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB ( Rotate (f,p))),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB ( Rotate (f,p))),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k)) = ( cell (( GoB ( Rotate (f,p))),i1,j2))

      proof

        

         A12: ( left_cell (f,k)) = ( left_cell (f,k));

        let i1,j1,i2,j2 be Nat such that

         A13: [i1, j1] in ( Indices ( GoB ( Rotate (f,p)))) & [i2, j2] in ( Indices ( GoB ( Rotate (f,p)))) and

         A14: (( Rotate (f,p)) /. n) = (( GoB ( Rotate (f,p))) * (i1,j1)) & (( Rotate (f,p)) /. (n + 1)) = (( GoB ( Rotate (f,p))) * (i2,j2));

        

         A15: ( GoB ( Rotate (f,p))) = ( GoB f) by Th28;

        then

         A16: (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) by A1, A2, A3, A6, A8, A10, A14, Th18;

        then

         A17: i1 = i2 & (j1 + 1) = j2 & ( left_cell (f,k)) = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & ( left_cell (f,k)) = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A2, A5, A13, A15, A12, GOBOARD5:def 7;

        per cases by A2, A5, A13, A15, A16, A12, GOBOARD5:def 7;

          case i1 = i2 & (j1 + 1) = j2;

          hence thesis by A17, Th28;

        end;

          case (i1 + 1) = i2 & j1 = j2;

          hence thesis by A17, Th28;

        end;

          case i1 = (i2 + 1) & j1 = j2;

          hence thesis by A17, Th28;

        end;

          case i1 = i2 & j1 = (j2 + 1);

          hence thesis by A17, Th28;

        end;

      end;

      (1 + (p .. f)) <= (k + ( len f)) by A2, A4, XREAL_1: 7;

      then 1 <= n by NAT_D: 55;

      hence thesis by A9, A11, GOBOARD5:def 7;

    end;

    theorem :: REVROT_1:36

    

     Th36: for f be non constant standard special_circular_sequence holds ( LeftComp ( Rotate (f,p))) = ( LeftComp f)

    proof

      let f be non constant standard special_circular_sequence;

      

       A1: p in ( rng f) implies (p .. f) >= 1 by FINSEQ_4: 21;

      ( LeftComp ( Rotate (f,p))) is_a_component_of (( L~ ( Rotate (f,p))) ` ) by GOBOARD9:def 1;

      then

       A2: ( LeftComp ( Rotate (f,p))) is_a_component_of (( L~ f) ` ) by Th33;

      per cases by A1, XXREAL_0: 1;

        suppose not p in ( rng f);

        hence thesis by FINSEQ_6:def 2;

      end;

        suppose p in ( rng f) & (p .. f) = 1;

        then 1 in ( dom f) & (f . 1) = p by FINSEQ_4: 19, FINSEQ_5: 6;

        then (f /. 1) = p by PARTFUN1:def 6;

        hence thesis by FINSEQ_6: 89;

      end;

        suppose that

         A3: p in ( rng f) and

         A4: 1 < (p .. f);

        

         A5: (p .. f) <= ( len f) by A3, FINSEQ_4: 21;

        then

         A6: (1 + (p .. f)) <= (1 + ( len f)) by XREAL_1: 6;

        (1 + 1) <= (p .. f) by A4, NAT_1: 13;

        then ((1 + 1) + ( len f)) <= (( len f) + (p .. f)) by XREAL_1: 6;

        then ( len f) <= (( len f) + 1) & (((1 + ( len f)) + 1) -' (p .. f)) <= ( len f) by NAT_1: 11, NAT_D: 53;

        then (((1 + ( len f)) -' (p .. f)) + 1) <= ( len f) by A5, NAT_D: 38, XXREAL_0: 2;

        then

         A7: (((1 + ( len f)) -' (p .. f)) + 1) <= ( len ( Rotate (f,p))) by Th14;

        ( left_cell (f,1)) = ( left_cell (( Rotate (f,p)),((1 + ( len f)) -' (p .. f)))) by A3, A4, Th35;

        then ( Int ( left_cell (f,1))) c= ( LeftComp ( Rotate (f,p))) by A6, A7, GOBOARD9: 21, NAT_D: 55;

        hence thesis by A2, GOBOARD9:def 1;

      end;

    end;

    theorem :: REVROT_1:37

    for f be non constant standard special_circular_sequence holds ( RightComp ( Rotate (f,p))) = ( RightComp f)

    proof

      let f be non constant standard special_circular_sequence;

      

       A1: ( RightComp f) = ( LeftComp ( Rev f)) by GOBOARD9: 23;

      ( RightComp ( Rotate (f,p))) = ( LeftComp ( Rev ( Rotate (f,p)))) by GOBOARD9: 23

      .= ( LeftComp ( Rotate (( Rev f),p))) by Th29;

      hence thesis by A1, Th36;

    end;

    begin

    

     Lm1: for f be non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds f is clockwise_oriented or ( Rev f) is clockwise_oriented

    proof

      let f be non constant standard special_circular_sequence such that

       A1: (f /. 1) = ( N-min ( L~ f));

      ((1 + 1) + 1) < ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      then

       A2: 2 < (( len f) -' 1) by NAT_D: 52;

      

       A3: [( i_w_n f), ( width ( GoB f))] in ( Indices ( GoB f)) by JORDAN5D:def 7;

      then

       A4: ( i_w_n f) <= ( len ( GoB f)) by MATRIX_0: 32;

      

       A5: 1 <= ( width ( GoB f)) by A3, MATRIX_0: 32;

      

       A6: (( GoB f) * (( i_w_n f),( width ( GoB f)))) = ( N-min ( L~ f)) by JORDAN5D:def 7;

      

       A7: ( len f) > (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      then

       A8: (1 + 1) in ( dom f) by FINSEQ_3: 25;

      then

      consider i1,j1 be Nat such that

       A9: [i1, j1] in ( Indices ( GoB f)) and

       A10: (f /. 2) = (( GoB f) * (i1,j1)) by GOBOARD5: 11;

      

       A11: j1 <= ( width ( GoB f)) by A9, MATRIX_0: 32;

      

       A12: 1 <= j1 by A9, MATRIX_0: 32;

      then

       A13: 1 <= ( width ( GoB f)) by A11, XXREAL_0: 2;

      

       A14: 1 <= i1 by A9, MATRIX_0: 32;

      

       A15: i1 <= ( len ( GoB f)) by A9, MATRIX_0: 32;

       A16:

      now

        assume

         A17: ( width ( GoB f)) = j1;

        then ((( GoB f) * (1,j1)) `2 ) = ( N-bound ( L~ f)) by JORDAN5D: 40;

        then ((( GoB f) * (i1,j1)) `2 ) = ( N-bound ( L~ f)) by A12, A11, A14, A15, GOBOARD5: 1;

        then (( GoB f) * (i1,j1)) in ( N-most ( L~ f)) by A7, A8, A10, GOBOARD1: 1, SPRECT_2: 10;

        then (( N-min ( L~ f)) `1 ) <= ((( GoB f) * (i1,j1)) `1 ) by PSCOMP_1: 39;

        hence ( i_w_n f) <= i1 by A6, A12, A4, A14, A17, GOBOARD5: 3;

      end;

      

       A18: ( len f) > 1 by GOBOARD7: 34, XXREAL_0: 2;

      then

       A19: ( len f) in ( dom f) by FINSEQ_3: 25;

      1 in ( dom f) by A18, FINSEQ_3: 25;

      then ( |.(( i_w_n f) - i1).| + |.(( width ( GoB f)) - j1).|) = 1 by A1, A3, A6, A8, A9, A10, GOBOARD5: 12;

      then |.(( i_w_n f) - i1).| = 1 & ( width ( GoB f)) = j1 or |.(( width ( GoB f)) - j1).| = 1 & ( i_w_n f) = i1 by SEQM_3: 42;

      then

       A20: i1 = (( i_w_n f) + 1) & ( width ( GoB f)) = j1 or ( width ( GoB f)) = (j1 + 1) & ( i_w_n f) = i1 by A11, A16, SEQM_3: 41;

      ( i_e_n f) <= ( len ( GoB f)) by JORDAN5D: 45;

      then ( i_w_n f) < ( len ( GoB f)) by SPRECT_3: 27, XXREAL_0: 2;

      then

       A21: 1 <= (( i_w_n f) + 1) & (( i_w_n f) + 1) <= ( len ( GoB f)) by NAT_1: 11, NAT_1: 13;

      

       A22: (( len f) -' 1) <= ( len f) by NAT_D: 44;

      1 <= (( len f) -' 1) by A7, NAT_D: 55;

      then

       A23: (( len f) -' 1) in ( dom f) by A22, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A24: [i2, j2] in ( Indices ( GoB f)) and

       A25: (f /. (( len f) -' 1)) = (( GoB f) * (i2,j2)) by GOBOARD5: 11;

      

       A26: j2 <= ( width ( GoB f)) by A24, MATRIX_0: 32;

      

       A27: 1 <= i2 by A24, MATRIX_0: 32;

      

       A28: 1 <= j2 & i2 <= ( len ( GoB f)) by A24, MATRIX_0: 32;

       A29:

      now

        assume

         A30: ( width ( GoB f)) = j2;

        then ((( GoB f) * (1,j2)) `2 ) = ( N-bound ( L~ f)) by JORDAN5D: 40;

        then ((( GoB f) * (i2,j2)) `2 ) = ( N-bound ( L~ f)) by A26, A27, A28, GOBOARD5: 1;

        then (( GoB f) * (i2,j2)) in ( N-most ( L~ f)) by A7, A23, A25, GOBOARD1: 1, SPRECT_2: 10;

        then (( N-min ( L~ f)) `1 ) <= ((( GoB f) * (i2,j2)) `1 ) by PSCOMP_1: 39;

        hence ( i_w_n f) <= i2 by A6, A4, A27, A13, A30, GOBOARD5: 3;

      end;

      

       A31: ( len f) > 4 by GOBOARD7: 34;

      then

       A32: (( GoB f) * (i2,j2)) in ( L~ f) by A23, A25, GOBOARD1: 1, XXREAL_0: 2;

      

       A33: ((( len f) -' 1) + 1) = ( len f) by A31, XREAL_1: 235, XXREAL_0: 2;

      then (f /. ((( len f) -' 1) + 1)) = (f /. 1) by FINSEQ_6:def 1;

      then ( |.(i2 - ( i_w_n f)).| + |.(j2 - ( width ( GoB f))).|) = 1 by A1, A23, A3, A6, A24, A25, A19, A33, GOBOARD5: 12;

      then |.(i2 - ( i_w_n f)).| = 1 & j2 = ( width ( GoB f)) or |.(j2 - ( width ( GoB f))).| = 1 & i2 = ( i_w_n f) by SEQM_3: 42;

      then i2 = (( i_w_n f) + 1) & j2 = ( width ( GoB f)) or (j2 + 1) = ( width ( GoB f)) & i2 = ( i_w_n f) by A26, A29, SEQM_3: 41;

      then ((f /. 2) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) or ((f /. (( len f) -' 1)) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A22, A10, A25, A5, A20, A21, A2, GOBOARD5: 1, GOBOARD7: 37;

      then ((f /. 2) `2 ) = ( N-bound ( L~ f)) or ((f /. (( len f) -' 1)) `2 ) = ( N-bound ( L~ f)) by JORDAN5D: 40;

      then

       A34: (f /. 2) in ( N-most ( L~ f)) or (f /. (( len f) -' 1)) in ( N-most ( L~ f)) by A7, A8, A25, A32, GOBOARD1: 1, SPRECT_2: 10;

      reconsider A = ( L~ ( Rev f)) as non empty compact Subset of ( TOP-REAL 2);

      

       A35: A = ( L~ f) by SPPOL_2: 22;

      ((( len f) -' 1) + (1 + 1)) = (((( len f) -' 1) + 1) + 1)

      .= (( len f) + 1) by A31, XREAL_1: 235, XXREAL_0: 2;

      then

       A36: (( Rev f) /. 2) = (f /. (( len f) -' 1)) by A23, FINSEQ_5: 66;

      (( Rev f) /. 1) = (f /. ( len f)) by FINSEQ_5: 65

      .= ( N-min ( L~ f)) by A1, FINSEQ_6:def 1

      .= ( N-min A) by SPPOL_2: 22;

      hence thesis by A1, A36, A35, A34, SPRECT_2: 30;

    end;

    registration

      let p be Point of ( TOP-REAL 2);

      let f be clockwise_oriented non constant standard special_circular_sequence;

      cluster ( Rotate (f,p)) -> clockwise_oriented;

      coherence

      proof

        

         A1: for i st 1 < i & i < ( len f) holds (f /. i) <> (f /. 1) by GOBOARD7: 36;

        

         A2: ( L~ ( Rotate (f,p))) = ( L~ f) by Th33;

        per cases ;

          suppose

           A3: ( N-min ( L~ f)) = (f /. 1);

          then ( Rotate (( Rotate (f,p)),( N-min ( L~ f)))) = f by A1, Th16;

          hence (( Rotate (( Rotate (f,p)),( N-min ( L~ ( Rotate (f,p)))))) /. 2) in ( N-most ( L~ ( Rotate (f,p)))) by A2, A3, SPRECT_2: 30;

        end;

          suppose

           A4: ( N-min ( L~ f)) <> (f /. 1);

          

           A5: f just_once_values ( N-min ( L~ f))

          proof

            take ( n_w_n f);

            (( n_w_n f) + 1) <= ( len f) by JORDAN5D:def 15;

            then

             A6: ( n_w_n f) < ( len f) by NAT_1: 13;

            

             A7: 1 <= ( n_w_n f) by JORDAN5D:def 15;

            hence

             A8: ( n_w_n f) in ( dom f) by A6, FINSEQ_3: 25;

            

            thus

             A9: ( N-min ( L~ f)) = (f . ( n_w_n f)) by JORDAN5D:def 15

            .= (f /. ( n_w_n f)) by A8, PARTFUN1:def 6;

            let z be set;

            assume

             A10: z in ( dom f);

            then

            reconsider k = z as Element of NAT ;

            assume

             A11: z <> ( n_w_n f);

            per cases by A11, XXREAL_0: 1;

              suppose

               A12: k < ( n_w_n f);

              1 <= k by A10, FINSEQ_3: 25;

              hence thesis by A6, A9, A12, GOBOARD7: 36;

            end;

              suppose

               A13: k > ( n_w_n f);

              1 < ( n_w_n f) & k <= ( len f) by A4, A7, A9, A10, FINSEQ_3: 25, XXREAL_0: 1;

              hence thesis by A9, A13, GOBOARD7: 37;

            end;

          end;

          (( Rotate (f,( N-min ( L~ f)))) /. 2) in ( N-most ( L~ f)) by SPRECT_2:def 4;

          hence (( Rotate (( Rotate (f,p)),( N-min ( L~ ( Rotate (f,p)))))) /. 2) in ( N-most ( L~ ( Rotate (f,p)))) by A2, A5, FINSEQ_6: 105;

        end;

      end;

    end

    theorem :: REVROT_1:38

    for f be non constant standard special_circular_sequence holds f is clockwise_oriented or ( Rev f) is clockwise_oriented

    proof

      let f be non constant standard special_circular_sequence;

      per cases ;

        suppose ( N-min ( L~ f)) = (f /. 1);

        hence thesis by Lm1;

      end;

        suppose

         A1: ( N-min ( L~ f)) <> (f /. 1);

        thus thesis

        proof

          set g = ( Rotate (f,( N-min ( L~ f))));

          

           A2: for i st 1 < i & i < ( len f) holds (f /. i) <> (f /. 1) by GOBOARD7: 36;

          ( N-min ( L~ f)) in ( rng f) & ( L~ f) = ( L~ g) by Th33, SPRECT_2: 39;

          then

           A3: (g /. 1) = ( N-min ( L~ g)) by FINSEQ_6: 92;

          per cases by A3, Lm1;

            suppose g is clockwise_oriented;

            then

            reconsider g as clockwise_oriented non constant standard special_circular_sequence;

            f = ( Rotate (g,(f /. 1))) by A2, Th16;

            hence thesis;

          end;

            suppose ( Rev g) is clockwise_oriented;

            then

            reconsider h = ( Rev g) as clockwise_oriented non constant standard special_circular_sequence;

            

             A4: g just_once_values (f /. 1)

            proof

              take ((f /. 1) .. g);

              ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

              then

               A5: (f /. 1) <> (g /. 1) by A1, FINSEQ_6: 92;

              (f /. 1) in ( rng f) by FINSEQ_6: 42;

              then

               A6: (f /. 1) in ( rng g) by FINSEQ_6: 90, SPRECT_2: 39;

              hence

               A7: ((f /. 1) .. g) in ( dom g) by FINSEQ_4: 20;

              

              thus

               A8: (f /. 1) = (g . ((f /. 1) .. g)) by A6, FINSEQ_4: 19

              .= (g /. ((f /. 1) .. g)) by A7, PARTFUN1:def 6;

              let z be set such that

               A9: z in ( dom g) and

               A10: z <> ((f /. 1) .. g);

              reconsider k = z as Element of NAT by A9;

              per cases by A10, XXREAL_0: 1;

                suppose

                 A11: k < ((f /. 1) .. g);

                ((f /. 1) .. g) <= ( len g) & ((f /. 1) .. g) <> ( len g) by A6, A5, A8, FINSEQ_4: 21, FINSEQ_6:def 1;

                then

                 A12: ((f /. 1) .. g) < ( len g) by XXREAL_0: 1;

                1 <= k by A9, FINSEQ_3: 25;

                hence thesis by A8, A11, A12, GOBOARD7: 36;

              end;

                suppose

                 A13: k > ((f /. 1) .. g);

                ((f /. 1) .. g) >= 1 by A6, FINSEQ_4: 21;

                then

                 A14: ((f /. 1) .. g) > 1 by A5, A8, XXREAL_0: 1;

                k <= ( len g) by A9, FINSEQ_3: 25;

                hence thesis by A8, A13, A14, GOBOARD7: 37;

              end;

            end;

            ( Rev f) = ( Rev ( Rotate (g,(f /. 1)))) by A2, Th16

            .= ( Rotate (h,(f /. 1))) by A4, FINSEQ_6: 106;

            hence thesis;

          end;

        end;

      end;

    end;