:: Some Remarks on Clockwise Oriented Sequences on Go-boards
::  by Adam Naumowicz and Robert Milewski
::
:: Received March 1, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, PSCOMP_1,
      TOPREAL1, JORDAN9, FINSEQ_4, XXREAL_0, PARTFUN1, ARYTM_3, FUNCT_1,
      GOBOARD5, PRE_TOPC, RELAT_1, FINSEQ_6, FINSEQ_1, MATRIX_1, GOBOARD2,
      ARYTM_1, XBOOLE_0, JORDAN8, TREES_1, GOBOARD1, MCART_1, COMPLEX1, CARD_1,
      RLTOPSP1, TARSKI, SPRECT_2, GOBOARD9, JORDAN2C, TOPS_1, REAL_1, JORDAN5D,
      CONNSP_1, TOPREAL2, JORDAN1A, JORDAN6, JORDAN1E, SEQ_4, XXREAL_2, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
      XREAL_0, REAL_1, NAT_1, FUNCT_1, NAT_D, RELSET_1, PARTFUN1, FINSEQ_1,
      FINSEQ_4, MATRIX_0, FINSEQ_6, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1,
      TOPREAL2, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1,
      SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13,
      SPPOL_1, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN5D, JORDAN1A,
      JORDAN1E, XXREAL_0;
 constructors REAL_1, FINSEQ_4, NEWTON, TOPS_1, CONNSP_1, GOBOARD2, PSCOMP_1,
      GOBOARD9, JORDAN6, JORDAN5D, JORDAN2C, JORDAN8, GOBRD13, JORDAN9,
      JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1;
 registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, GOBOARD2,
      SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, FUNCT_1,
      EUCLID, JORDAN2C, XREAL_0;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Preliminaries

reserve i,j,k,n for Nat;

theorem :: JORDAN1I:1
  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:2
  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:3
  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:4
  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:5
  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:6
  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:7
  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:8
  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:9
  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:10
  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:11
  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:12
  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:13
  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:14
  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: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,j) & f/.(k+1) = G*(i+1,j) holds j > 1;

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+1) & f/.(k+1) = G*(i,j) holds i > 1;

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+1,j) & f/.(k+1) = G*(i,j) holds (f/.k)`2 <> N-bound L~f
;

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) & f/.(k+1) = G*(i,j+1) holds (f/.k)`1 <> E-bound L~f
;

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,j) & f/.(k+1) = G*(i+1,j) holds (f/.k)`2 <> S-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+1) & f/.(k+1) = G*(i,j) holds (f/.k)`1 <> W-bound L~f
;

theorem :: JORDAN1I:21
  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:22
  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: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 = 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: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 = 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:25
  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:26
  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:27
  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:28
  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
 = upper_bound(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);