Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

Again on the Order on a Special Polygon

by
Andrzej Trybulec, and
Yatsuka Nakamura

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;
```