The abstract of the Mizar article:

Again on the Order on a Special Polygon

by

Andrzej Trybulec, and

Yatsuka Nakamura

Received October 16, 2000

MML identifier: SPRECT_5

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FINSEQ_6, RELAT_1, FINSEQ_4, FINSEQ_5, ARYTM_1, RFINSEQ,
      BOOLE, SEQM_3, GOBOARD5, PRE_TOPC, EUCLID, FUNCT_1, RLSUB_2, PSCOMP_1,
      TOPREAL1, SPRECT_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, FUNCT_1, FINSEQ_1,
      FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6, NAT_1, BINARITH, PRE_TOPC, EUCLID,
      TOPREAL1, GOBOARD1, GOBOARD5, PSCOMP_1, SPRECT_2;
 constructors PSCOMP_1, GOBOARD5, BINARITH, REALSET1, FINSEQ_5, SEQM_3,
      FINSEQ_4, SPRECT_2, RFINSEQ;
 clusters RELSET_1, XREAL_0, ARYTM_3, SPRECT_2, FINSEQ_6, REVROT_1, SPRECT_1,
      XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve i for Nat,
        D for non empty set,
        f for FinSequence of D,
        g for circular FinSequence of D,
        p,p1,p2,p3,q for Element of D;

theorem :: SPRECT_5:1
 q in rng(f|(p..f)) implies q..f <= p..f;

theorem :: SPRECT_5:2
 p in rng f & q in rng f & p..f <= q..f
  implies q..(f:-p) = q..f - p..f + 1;

theorem :: SPRECT_5:3
 p in rng f & q in rng f & p..f <= q..f
  implies p..(f-:q) = p..f;

theorem :: SPRECT_5:4
 p in rng f & q in rng f & p..f <= q..f
  implies q..Rotate(f,p) = q..f - p..f + 1;

theorem :: SPRECT_5:5
 p1 in rng f & p2 in rng f & p3 in rng f &
 p1..f <= p2..f & p2..f < p3..f implies
   p2..Rotate(f,p1) < p3..Rotate(f,p1);

theorem :: SPRECT_5:6
   p1 in rng f & p2 in rng f & p3 in rng f &
 p1..f < p2..f & p2..f <= p3..f implies
   p2..Rotate(f,p1) <= p3..Rotate(f,p1);

theorem :: SPRECT_5:7
 p in rng g & len g > 1 implies p..g < len g;

begin :: Ordering of special points on a standard special sequence

reserve f for non constant standard special_circular_sequence,
        p,p1,p2,p3,q for Point of TOP-REAL 2;

theorem :: SPRECT_5:8
  f/^1 is one-to-one;

theorem :: SPRECT_5:9
 1 < q..f & q in rng f implies (f/.1)..Rotate(f,q) = len f + 1 - q..f;

theorem :: SPRECT_5:10
 p in rng f & q in rng f & p..f < q..f
  implies p..Rotate(f,q) = len f + p..f - q..f;

theorem :: SPRECT_5:11
 p1 in rng f & p2 in rng f & p3 in rng f &
 p1..f < p2..f & p2..f < p3..f implies
   p3..Rotate(f,p2) < p1..Rotate(f,p2);

theorem :: SPRECT_5:12
 p1 in rng f & p2 in rng f & p3 in rng f &
 p1..f < p2..f & p2..f < p3..f implies
   p1..Rotate(f,p3) < p2..Rotate(f,p3);

theorem :: SPRECT_5:13
   p1 in rng f & p2 in rng f & p3 in rng f &
 p1..f <= p2..f & p2..f < p3..f implies
   p1..Rotate(f,p3) <= p2..Rotate(f,p3);

theorem :: SPRECT_5:14
   (S-min L~f)..f < len f;

theorem :: SPRECT_5:15
   (S-max L~f)..f < len f;

theorem :: SPRECT_5:16
   (E-min L~f)..f < len f;

theorem :: SPRECT_5:17
   (E-max L~f)..f < len f;

theorem :: SPRECT_5:18
   (N-min L~f)..f < len f;

theorem :: SPRECT_5:19
   (N-max L~f)..f < len f;

theorem :: SPRECT_5:20
   (W-max L~f)..f < len f;

theorem :: SPRECT_5:21
   (W-min L~f)..f < len f;

begin :: Ordering of special points on a clockwise oriented sequence

reserve z for clockwise_oriented
              (non constant standard special_circular_sequence);

theorem :: SPRECT_5:22
 f/.1 = W-min L~f implies (W-min L~f)..f < (W-max L~f)..f;

theorem :: SPRECT_5:23
   f/.1 = W-min L~f implies (W-max L~f)..f > 1;

theorem :: SPRECT_5:24
 z/.1 = W-min L~z & W-max L~z <> N-min L~z
  implies (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:25
 z/.1 = W-min L~z implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:26
 z/.1 = W-min L~z & N-max L~z <> E-max L~z implies
  (N-max L~z)..z < (E-max L~z)..z;

theorem :: SPRECT_5:27
 z/.1 = W-min L~z implies (E-max L~z)..z < (E-min L~z)..z;

theorem :: SPRECT_5:28
 z/.1 = W-min L~z & E-min L~z <> S-max L~z implies
  (E-min L~z)..z < (S-max L~z)..z;

theorem :: SPRECT_5:29
   z/.1 = W-min L~z & S-min L~z <> W-min L~z
  implies (S-max L~z)..z < (S-min L~z)..z;

theorem :: SPRECT_5:30
 f/.1 = S-max L~f implies (S-max L~f)..f < (S-min L~f)..f;

theorem :: SPRECT_5:31
   f/.1 = S-max L~f implies (S-min L~f)..f > 1;

theorem :: SPRECT_5:32
 z/.1 = S-max L~z & S-min L~z <> W-min L~z
  implies (S-min L~z)..z < (W-min L~z)..z;

theorem :: SPRECT_5:33
 z/.1 = S-max L~z implies (W-min L~z)..z < (W-max L~z)..z;

theorem :: SPRECT_5:34
 z/.1 = S-max L~z & W-max L~z <> N-min L~z implies
  (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:35
 z/.1 = S-max L~z implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:36
 z/.1 = S-max L~z & N-max L~z <> E-max L~z implies
  (N-max L~z)..z < (E-max L~z)..z;

theorem :: SPRECT_5:37
   z/.1 = S-max L~z & E-min L~z <> S-max L~z
  implies (E-max L~z)..z < (E-min L~z)..z;

theorem :: SPRECT_5:38
 f/.1 = E-max L~f implies (E-max L~f)..f < (E-min L~f)..f;

theorem :: SPRECT_5:39
   f/.1 = E-max L~f implies (E-min L~f)..f > 1;

theorem :: SPRECT_5:40
 z/.1 = E-max L~z & S-max L~z <> E-min L~z
  implies (E-min L~z)..z < (S-max L~z)..z;

theorem :: SPRECT_5:41
 z/.1 = E-max L~z implies (S-max L~z)..z < (S-min L~z)..z;

theorem :: SPRECT_5:42
 z/.1 = E-max L~z & S-min L~z <> W-min L~z implies
  (S-min L~z)..z < (W-min L~z)..z;

theorem :: SPRECT_5:43
 z/.1 = E-max L~z implies (W-min L~z)..z < (W-max L~z)..z;

theorem :: SPRECT_5:44
 z/.1 = E-max L~z & W-max L~z <> N-min L~z implies
  (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:45
   z/.1 = E-max L~z & N-max L~z <> E-max L~z
  implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:46
   f/.1 = N-max L~f & N-max L~f <> E-max L~f
    implies (N-max L~f)..f < (E-max L~f)..f;

theorem :: SPRECT_5:47
   z/.1 = N-max L~z implies (E-max L~z)..z < (E-min L~z)..z;

theorem :: SPRECT_5:48
   z/.1 = N-max L~z & E-min L~z <> S-max L~z
  implies (E-min L~z)..z < (S-max L~z)..z;

theorem :: SPRECT_5:49
   z/.1 = N-max L~z implies (S-max L~z)..z < (S-min L~z)..z;

theorem :: SPRECT_5:50
   z/.1 = N-max L~z & S-min L~z <> W-min L~z
  implies (S-min L~z)..z < (W-min L~z)..z;

theorem :: SPRECT_5:51
   z/.1 = N-max L~z implies (W-min L~z)..z < (W-max L~z)..z;

theorem :: SPRECT_5:52
   z/.1 = N-max L~z & N-min L~z <> W-max L~z
  implies (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:53
   f/.1 = E-min L~f & E-min L~f <> S-max L~f
    implies (E-min L~f)..f < (S-max L~f)..f;

theorem :: SPRECT_5:54
   z/.1 = E-min L~z implies (S-max L~z)..z < (S-min L~z)..z;

theorem :: SPRECT_5:55
   z/.1 = E-min L~z & S-min L~z <> W-min L~z
  implies (S-min L~z)..z < (W-min L~z)..z;

theorem :: SPRECT_5:56
   z/.1 = E-min L~z implies (W-min L~z)..z < (W-max L~z)..z;

theorem :: SPRECT_5:57
   z/.1 = E-min L~z & W-max L~z <> N-min L~z
  implies (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:58
   z/.1 = E-min L~z implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:59
   z/.1 = E-min L~z & E-max L~z <> N-max L~z
  implies (N-max L~z)..z < (E-max L~z)..z;

theorem :: SPRECT_5:60
   f/.1 = S-min L~f & S-min L~f <> W-min L~f
    implies (S-min L~f)..f < (W-min L~f)..f;

theorem :: SPRECT_5:61
   z/.1 = S-min L~z implies (W-min L~z)..z < (W-max L~z)..z;

theorem :: SPRECT_5:62
   z/.1 = S-min L~z & W-max L~z <> N-min L~z
  implies (W-max L~z)..z < (N-min L~z)..z;

theorem :: SPRECT_5:63
   z/.1 = S-min L~z implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:64
   z/.1 = S-min L~z & N-max L~z <> E-max L~z
  implies (N-max L~z)..z < (E-max L~z)..z;

theorem :: SPRECT_5:65
   z/.1 = S-min L~z implies (E-max L~z)..z < (E-min L~z)..z;

theorem :: SPRECT_5:66
   z/.1 = S-min L~z & S-max L~z <> E-min L~z
  implies (E-min L~z)..z < (S-max L~z)..z;

theorem :: SPRECT_5:67
   f/.1 = W-max L~f & W-max L~f <> N-min L~f
    implies (W-max L~f)..f < (N-min L~f)..f;

theorem :: SPRECT_5:68
   z/.1 = W-max L~z implies (N-min L~z)..z < (N-max L~z)..z;

theorem :: SPRECT_5:69
   z/.1 = W-max L~z & N-max L~z <> E-max L~z
  implies (N-max L~z)..z < (E-max L~z)..z;

theorem :: SPRECT_5:70
   z/.1 = W-max L~z implies (E-max L~z)..z < (E-min L~z)..z;

theorem :: SPRECT_5:71
   z/.1 = W-max L~z & E-min L~z <> S-max L~z
  implies (E-min L~z)..z < (S-max L~z)..z;

theorem :: SPRECT_5:72
   z/.1 = W-max L~z implies (S-max L~z)..z < (S-min L~z)..z;

theorem :: SPRECT_5:73
   z/.1 = W-max L~z & W-min L~z <> S-min L~z
  implies (S-min L~z)..z < (W-min L~z)..z;