The abstract of the Mizar article:

Some Remarks on Clockwise Oriented Sequences on Go-boards

by

Adam Naumowicz, and

Robert Milewski

Received March 1, 2002

MML identifier: JORDAN1I

[ Mizar article, MML identifier index ]

environ

 vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
      JORDAN6, SPRECT_2, JORDAN2C, ABSVALUE, REALSET1, JORDAN1E, FINSEQ_4,
      TOPS_1, TOPREAL2, CONNSP_1, COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1,
      TREES_1, EUCLID, RELAT_1, MCART_1, MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2,
      SEQM_3, SUBSET_1, FUNCT_1, ARYTM_1, FINSEQ_6, GOBOARD2, ARYTM_3,
      ORDINAL2, FUNCT_5, JORDAN5D;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, REAL_1, NAT_1, ABSVALUE,
      FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, MATRIX_1, FINSEQ_6, REALSET1,
      STRUCT_0, PRE_TOPC, TOPS_1, TOPREAL2, BINARITH, CONNSP_1, COMPTS_1,
      EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5,
      GOBOARD9, GOBRD13, SPPOL_1, JORDAN8, JORDAN2C, JORDAN6, JORDAN9,
      JORDAN5D, JORDAN1A, JORDAN1E;
 constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
      BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, ABSVALUE, FINSEQ_4,
      GOBRD13, TOPREAL2, SPRECT_1, GOBOARD2, INT_1, TOPS_1, JORDAN1E, JORDAN5D;
 clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, SPRECT_3,
      GOBOARD2, JORDAN1A, MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Preliminaries

  reserve i,j,k,n for Nat;

  theorem :: JORDAN1I:1
   for A,B being Subset of TOP-REAL n holds
    A is Bounded or B is Bounded implies A /\ B is Bounded;

  theorem :: JORDAN1I:2
   for A,B being Subset of TOP-REAL n holds
    A is not Bounded & B is Bounded implies A \ B is not Bounded;

theorem :: JORDAN1I:3
 for C being compact connected non vertical non horizontal Subset of TOP-REAL 2
 holds (W-min L~Cage(C,n))..Cage(C,n) > 1;

theorem :: JORDAN1I:4
 for C being compact connected non vertical non horizontal Subset of TOP-REAL 2
 holds (E-max L~Cage(C,n))..Cage(C,n) > 1;

theorem :: JORDAN1I:5
 for C being compact connected non vertical non horizontal Subset of TOP-REAL 2
 holds (S-max L~Cage(C,n))..Cage(C,n) > 1;

begin :: On bounding points of circular sequences

theorem :: JORDAN1I:6
   for f being non constant standard special_circular_sequence,
 p being Point of TOP-REAL 2 st p in rng f holds
 left_cell(f,p..f) = left_cell(Rotate(f,p),1);

theorem :: JORDAN1I:7
 for f being non constant standard special_circular_sequence,
 p being Point of TOP-REAL 2 st p in rng f holds
 right_cell(f,p..f) = right_cell(Rotate(f,p),1);

theorem :: JORDAN1I:8
   for C being compact connected non vertical non horizontal non empty
 Subset of TOP-REAL 2 holds
 W-min C in right_cell(Rotate(Cage(C,n),W-min L~Cage(C,n)),1);

theorem :: JORDAN1I:9
   for C being compact connected non vertical non horizontal non empty
 Subset of TOP-REAL 2 holds
 E-max C in right_cell(Rotate(Cage(C,n),E-max L~Cage(C,n)),1);

theorem :: JORDAN1I:10
   for C being compact connected non vertical non horizontal non empty
 Subset of TOP-REAL 2 holds
 S-max C in right_cell(Rotate(Cage(C,n),S-max L~Cage(C,n)),1);

begin :: On clockwise oriented sequences

  theorem :: JORDAN1I:11
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for p being Point of TOP-REAL 2 st p`1 < W-bound (L~f) holds
   p in LeftComp f;

  theorem :: JORDAN1I:12
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for p being Point of TOP-REAL 2 st p`1 > E-bound (L~f) holds
    p in LeftComp f;

  theorem :: JORDAN1I:13
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for p being Point of TOP-REAL 2 st p`2 < S-bound (L~f) holds
    p in LeftComp f;

  theorem :: JORDAN1I:14
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for p being Point of TOP-REAL 2 st p`2 > N-bound (L~f) holds
    p in LeftComp f;

  theorem :: JORDAN1I:15
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in Indices G &
    f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) holds j < width G;

  theorem :: JORDAN1I:16
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in Indices G &
    f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) holds i < len G;

  theorem :: JORDAN1I:17
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in Indices G &
    f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) holds j > 1;

  theorem :: JORDAN1I:18
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in Indices G &
    f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) holds i > 1;

  theorem :: JORDAN1I:19
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in Indices G &
    f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j) holds (f/.k)`2 <> N-bound L~f;

  theorem :: JORDAN1I:20
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in Indices G &
    f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1) holds (f/.k)`1 <> E-bound L~f;

  theorem :: JORDAN1I:21
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i+1,j] in Indices G &
    f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j) holds (f/.k)`2 <> S-bound L~f;

  theorem :: JORDAN1I:22
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board st f is_sequence_on G
   for i,j,k being Nat st
    1 <= k & k+1 <= len f & [i,j] in Indices G & [i,j+1] in Indices G &
    f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j) holds (f/.k)`1 <> W-bound L~f;

  theorem :: JORDAN1I:23
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board for k being Nat st
   f is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = W-min L~f
   ex i,j be Nat st [i,j] in Indices G & [i,j+1] in Indices G &
   f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1);

  theorem :: JORDAN1I:24
     for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board for k being Nat st
    f is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = N-min L~f
   ex i,j be Nat st [i,j] in Indices G & [i+1,j] in Indices G &
   f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j);

  theorem :: JORDAN1I:25
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board for k being Nat st
    f is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = E-max L~f
   ex i,j be Nat st [i,j+1] in Indices G & [i,j] in Indices G &
   f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j);

  theorem :: JORDAN1I:26
   for f being clockwise_oriented non constant
   standard special_circular_sequence
   for G being Go-board for k being Nat st
    f is_sequence_on G & 1 <= k & k+1 <= len f & f/.k = S-max L~f
   ex i,j be Nat st [i+1,j] in Indices G & [i,j] in Indices G &
   f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j);

theorem :: JORDAN1I:27
   for f being non constant standard special_circular_sequence holds
 f is clockwise_oriented iff Rotate(f,W-min L~f)/.2 in W-most L~f;

theorem :: JORDAN1I:28
   for f being non constant standard special_circular_sequence holds
 f is clockwise_oriented iff Rotate(f,E-max L~f)/.2 in E-most L~f;

theorem :: JORDAN1I:29
   for f being non constant standard special_circular_sequence holds
 f is clockwise_oriented iff Rotate(f,S-max L~f)/.2 in S-most L~f;

theorem :: JORDAN1I:30
   for C being compact non vertical non horizontal non empty
 being_simple_closed_curve Subset of TOP-REAL 2
 for p being Point of TOP-REAL 2 holds
 p`1 = (W-bound C + E-bound C)/2 & i > 0 &
 1 <= k & k <= width Gauge(C,i) &
 Gauge(C,i)*(Center Gauge(C,i),k) in Upper_Arc L~Cage(C,i) &
 p`2 = sup(proj2.:(LSeg(Gauge(C,1)*(Center Gauge(C,1),1),
   Gauge(C,i)*(Center Gauge(C,i),k)) /\ Lower_Arc L~Cage(C,i)))
 implies
  ex j st 1 <= j & j <= width Gauge(C,i) & p = Gauge(C,i)*(Center Gauge(C,i),j)
;