The abstract of the Mizar article:

Rotating and Reversing

by

Andrzej Trybulec

Received January 21, 1999

MML identifier: REVROT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, REALSET1, SEQM_3, RELAT_1, FINSEQ_4, FUNCT_1, FINSEQ_5,
      RFINSEQ, BOOLE, ARYTM_1, FINSEQ_6, EUCLID, JORDAN2C, FINSEQ_2, GOBOARD1,
      MCART_1, PRE_TOPC, TOPREAL1, GOBOARD2, CARD_1, GOBOARD5, TARSKI,
      MATRIX_1, ABSVALUE, GOBOARD9, CONNSP_1, SUBSET_1, TOPS_1, PSCOMP_1,
      SPRECT_2, COMPTS_1, JORDAN5D, TREES_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, ABSVALUE,
      BINARITH, CARD_1, REALSET1, FUNCT_1, FINSEQ_1, FINSEQ_2, MATRIX_1,
      FINSEQ_4, RFINSEQ, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_1,
      CONNSP_1, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5,
      GOBOARD9, PSCOMP_1, JORDAN5D, SPRECT_2, JORDAN2C;
 constructors TOPS_1, GOBOARD9, SPRECT_2, PSCOMP_1, RFINSEQ, BINARITH, REAL_1,
      CONNSP_1, GOBOARD2, FINSEQ_4, INT_1, ABSVALUE, JORDAN5D, JORDAN2C,
      REALSET1, COMPTS_1, FINSEQOP;
 clusters RELSET_1, SPRECT_1, SPRECT_2, EUCLID, FINSEQ_6, FINSEQ_5, GOBOARD9,
      GOBOARD2, PSCOMP_1, INT_1, FINSEQ_1, TEX_1, REALSET1, BINARITH, MEMBERED;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin ::Preliminaries

reserve i,j,k,m,n for Nat,
        D for non empty set,
        p for Element of D,
        f for FinSequence of D;

definition let S be non trivial 1-sorted;
 cluster the carrier of S -> non trivial;
end;

definition let D be non empty set; let f be FinSequence of D;
redefine attr f is constant means
:: REVROT_1:def 1 :: GOBOARD1:def 2
 for n,m st n in dom f & m in dom f holds f/.n=f/.m;
end;

theorem :: REVROT_1:1
 for D being non empty set, f being FinSequence of D
  st f just_once_values f/.len f
 holds f/.len f..f = len f;

theorem :: REVROT_1:2
 for D being non empty set, f being FinSequence of D
 holds f /^ len f = {};

theorem :: REVROT_1:3
 for D being non empty set, f being non empty FinSequence of D
  holds f/.len f in rng f;

definition let D be non empty set, f be FinSequence of D, y be set;
 redefine pred f just_once_values y means
:: REVROT_1:def 2
    ex x being set st x in dom f & y = f/.x &
   for z being set st z in dom f & z <> x holds f/.z <> y;
end;

theorem :: REVROT_1:4
 for D being non empty set, f being FinSequence of D
  st f just_once_values f/.len f
 holds f-:f/.len f = f;

theorem :: REVROT_1:5
 for D being non empty set, f being FinSequence of D
  st f just_once_values f/.len f
 holds f:-f/.len f = <*f/.len f*>;

theorem :: REVROT_1:6
 1 <= len (f:-p);

theorem :: REVROT_1:7
   for D being non empty set, p being Element of D, f being FinSequence of D
   st p in rng f
  holds len(f:-p) <= len f;

theorem :: REVROT_1:8
   for D being non empty set, f being circular non empty FinSequence of D
 holds Rev f is circular;

begin :: About Rotation

reserve D for non empty set,
        p for Element of D,
        f for FinSequence of D;

theorem :: REVROT_1:9
 p in rng f & 1 <= i & i <= len(f:-p)
 implies (Rotate(f,p))/.i = f/.(i -' 1 + p..f);

theorem :: REVROT_1:10
 p in rng f & p..f <= i & i <= len f
 implies f/.i = (Rotate(f,p))/.(i+1 -' p..f);

theorem :: REVROT_1:11
 p in rng f implies (Rotate(f,p))/.len(f:-p) = f/.len f;

theorem :: REVROT_1:12
 p in rng f & len(f:-p) < i & i <= len f
 implies (Rotate(f,p))/.i = f/.(i + p..f -' len f);

theorem :: REVROT_1:13
   p in rng f & 1 < i & i <= p..f
 implies f/.i = (Rotate(f,p))/.(i + len f -' p..f);

theorem :: REVROT_1:14
 len Rotate(f,p) = len f;

theorem :: REVROT_1:15
 dom Rotate(f,p) = dom f;

theorem :: REVROT_1:16
 for D being non empty set, f being 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;

begin :: Rotating circular

reserve f for circular FinSequence of D;

theorem :: REVROT_1:17
 p in rng f & len(f:-p) <= i & i <= len f
 implies (Rotate(f,p))/.i = f/.(i + p..f -' len f);

theorem :: REVROT_1:18
 p in rng f & 1 <= i & i <= p..f
 implies f/.i = (Rotate(f,p))/.(i + len f -' p..f);

definition let D be non trivial set;
 cluster non constant circular FinSequence of D;
end;

definition let D be non trivial set, p be Element of D;
 let f be non constant circular FinSequence of D;
 cluster Rotate(f,p) -> non constant;
end;

begin :: Finite sequences on the plane

theorem :: REVROT_1:19
 for n being non empty Nat holds
  0.REAL n <> 1.REAL n;

definition let n be non empty Nat;
 cluster TOP-REAL n -> non trivial;
end;

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

theorem :: REVROT_1:20
 rng f c= rng g implies rng X_axis f c= rng X_axis g;

theorem :: REVROT_1:21
 rng f = rng g implies rng X_axis f = rng X_axis g;

theorem :: REVROT_1:22
 rng f c= rng g implies rng Y_axis f c= rng Y_axis g;

theorem :: REVROT_1:23
 rng f = rng g implies rng Y_axis f = rng Y_axis g;

begin :: Rotating finite sequences on the plane

reserve p for Point of TOP-REAL 2,
        f for FinSequence of TOP-REAL 2;

definition let p be Point of TOP-REAL 2;
 let f be special circular FinSequence of TOP-REAL 2;
 cluster Rotate(f,p) -> special;
end;

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

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

theorem :: REVROT_1:26
 for f being circular FinSequence of TOP-REAL 2
  holds Incr X_axis f = Incr X_axis Rotate(f,p);

theorem :: REVROT_1:27
 for f being circular FinSequence of TOP-REAL 2
 holds Incr Y_axis f = Incr Y_axis Rotate(f,p);

theorem :: REVROT_1:28
 for f being non empty circular FinSequence of TOP-REAL 2
  holds GoB Rotate(f,p) = GoB f;

theorem :: REVROT_1:29
 for f being non constant standard special_circular_sequence
 holds Rev Rotate(f,p) = Rotate(Rev f,p);

begin :: Circular finite sequences of points of the plane

reserve f for circular FinSequence of TOP-REAL 2;

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

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

definition 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.;
end;

definition let p be Point of TOP-REAL 2;
 let f be non constant standard special_circular_sequence;
 cluster Rotate(f,p) -> unfolded;
end;

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

theorem :: REVROT_1:33
 L~Rotate(f,p) = L~f;

theorem :: REVROT_1:34
 for G being Go-board holds
  f is_sequence_on G iff Rotate(f,p) is_sequence_on G;

definition 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;
end;

theorem :: REVROT_1:35
 for f being 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);

theorem :: REVROT_1:36
 for f being non constant standard special_circular_sequence
 holds LeftComp Rotate(f,p) = LeftComp f;

theorem :: REVROT_1:37
   for f being non constant standard special_circular_sequence
 holds RightComp Rotate(f,p) = RightComp f;

begin

definition 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;
end;

theorem :: REVROT_1:38
   for f being non constant standard special_circular_sequence
 holds f is clockwise_oriented or Rev f is clockwise_oriented;