Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

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

Back to top