:: Some Properties of Cells and Arcs
::  by Robert Milewski , Andrzej Trybulec , Artur Korni{\l}owicz
::   and Adam Naumowicz
::
:: Received October 6, 2000
:: Copyright (c) 2000-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, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, RELAT_2, GOBOARD1,
      PRE_TOPC, FINSEQ_1, XBOOLE_0, FINSEQ_5, XXREAL_0, JORDAN3, RELAT_1,
      TOPREAL1, FUNCT_1, GROUP_2, ORDINAL4, ARYTM_3, TOPREAL2, PSCOMP_1,
      ARYTM_1, PARTFUN1, CARD_1, NAT_1, RLTOPSP1, MCART_1, SPRECT_2, FINSEQ_6,
      FINSEQ_4, ZFMISC_1, JORDAN1A, INT_1, JORDAN8, NEWTON, TARSKI, GOBOARD5,
      TREES_1, REAL_1, JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, CONNSP_1, SEQ_4,
      XXREAL_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, REAL_1, COMPLEX1, INT_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1,
      FINSEQ_1, FINSEQ_4, NEWTON, FINSEQ_5, MATRIX_0, ZFMISC_1, FINSEQ_6,
      STRUCT_0, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID,
      PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, JORDAN3,
      JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A;
 constructors REAL_1, SQUARE_1, NAT_D, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5,
      CONNSP_1, MONOID_0, GOBOARD1, PSCOMP_1, JORDAN3, JORDAN6, JORDAN2C,
      JORDAN8, JORDAN9, JORDAN1A, CONVEX1, RELSET_1;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_5,
      STRUCT_0, MONOID_0, EUCLID, TOPREAL2, TOPREAL5, SPRECT_2, TOPREAL6,
      JORDAN8, FUNCT_1, RELAT_1, RLTOPSP1, SPPOL_2, JORDAN2C, ORDINAL1, NEWTON;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

reserve E for compact non vertical non horizontal Subset of TOP-REAL 2,
  C for compact connected non vertical non horizontal Subset of TOP-REAL 2,
  G for Go-board,
  i, j, m, n for Nat,
  p for Point of TOP-REAL 2;

theorem :: JORDAN1B:1
  for f being FinSequence holds f is empty iff Rev f is empty;

theorem :: JORDAN1B:2
  for D being non empty set, f being FinSequence of D for i,j st 1 <= i
  & i <= len f & 1 <= j & j <= len f holds mid(f,i,j) is non empty;

theorem :: JORDAN1B:3
  for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
  st 1 <= len f & p in L~f holds R_Cut(f,p).1 = f.1;

theorem :: JORDAN1B:4
  for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f
  is being_S-Seq & p in L~f holds L_Cut(f,p).(len L_Cut(f,p)) = f.(len f);

theorem :: JORDAN1B:5
  for P be Simple_closed_curve holds W-max(P) <> E-max(P);

theorem :: JORDAN1B:6
  for D be non empty set for f be FinSequence of D st 1 <= i & i < len f
  holds mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f);

theorem :: JORDAN1B:7
  for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is vertical holds
  <*p,q*> is being_S-Seq;

theorem :: JORDAN1B:8
  for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is horizontal
  holds <*p,q*> is being_S-Seq;

theorem :: JORDAN1B:9
  for p,q be FinSequence of TOP-REAL 2 for v be Point of TOP-REAL
  2 st p is_in_the_area_of q holds Rotate(p,v) is_in_the_area_of q;

theorem :: JORDAN1B:10
  for p be non trivial FinSequence of TOP-REAL 2 for v be Point of
  TOP-REAL 2 holds Rotate(p,v) is_in_the_area_of p;

theorem :: JORDAN1B:11
  for f be FinSequence holds Center f >= 1;

theorem :: JORDAN1B:12
  for f be FinSequence st len f >= 1 holds Center f <= len f;

theorem :: JORDAN1B:13
  Center G <= len G;

theorem :: JORDAN1B:14
  for f be FinSequence st len f >= 2 holds Center f > 1;

theorem :: JORDAN1B:15
  for f be FinSequence st len f >= 3 holds Center f < len f;

theorem :: JORDAN1B:16
  Center Gauge(E,n) = 2|^(n-'1) + 2;

theorem :: JORDAN1B:17
  E c= cell(Gauge(E,0),2,2);

theorem :: JORDAN1B:18
  not cell(Gauge(E,0),2,2) c= BDD E;

theorem :: JORDAN1B:19
  Gauge(C,1)*(Center Gauge(C,1),1) = |[(W-bound C + E-bound C)/2,S-bound
  L~Cage(C,1)]|;

theorem :: JORDAN1B:20
  Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1)) = |[(W-bound C + E-bound
  C)/2,N-bound L~Cage(C,1)]|;

theorem :: JORDAN1B:21
  1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width
  G & p in cell(G,len G,j) & p`1 = G*(m,n)`1 implies len G = m;

theorem :: JORDAN1B:22
  1 <= i & i <= len G & 1 <= j & j < width G & 1 <= m & m <= len G & 1
<= n & n <= width G & p in cell(G,i,j) & p`1 = G*(m,n)`1 implies i = m or i = m
  -' 1;

theorem :: JORDAN1B:23
  1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G
  & p in cell(G,i,width G) & p`2 = G*(m,n)`2 implies width G = n;

theorem :: JORDAN1B:24
  1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1
<= n & n <= width G & p in cell(G,i,j) & p`2 = G*(m,n)`2 implies j = n or j = n
  -' 1;

theorem :: JORDAN1B:25
  for C be Simple_closed_curve for i be Nat st 1 < i &
  i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
  meets Upper_Arc C;

theorem :: JORDAN1B:26
  for C be Simple_closed_curve for i be Nat st 1 < i &
  i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
  meets Lower_Arc C;

theorem :: JORDAN1B:27
  for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc C;

theorem :: JORDAN1B:28
  for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),
  1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc C;

theorem :: JORDAN1B:29
  for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(
  Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc L~Cage(C,n);

theorem :: JORDAN1B:30
  for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(
  Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc L~Cage(C,n);

theorem :: JORDAN1B:31
  for C be compact connected non vertical non horizontal Subset of
  TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center
  Gauge(C,n),len Gauge(C,n))) meets Upper_Arc L~Cage(C,n);

theorem :: JORDAN1B:32
  for C be compact connected non vertical non horizontal Subset of
  TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center
  Gauge(C,n),len Gauge(C,n))) meets Lower_Arc L~Cage(C,n);

theorem :: JORDAN1B:33
  j <= width G implies cell(G,0,j) is not bounded;

theorem :: JORDAN1B:34
  i <= width G implies cell(G,len G,i) is not bounded;

theorem :: JORDAN1B:35
  j <= width Gauge(C,n) implies cell(Gauge(C,n),0,j) c= UBD C;

theorem :: JORDAN1B:36
  j <= len Gauge(E,n) implies cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E;

theorem :: JORDAN1B:37
  i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
  j) c= BDD C implies j > 1;

theorem :: JORDAN1B:38
  i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
  j) c= BDD C implies i > 1;

theorem :: JORDAN1B:39
  i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
  j) c= BDD C implies j+1 < width Gauge(C,n);

theorem :: JORDAN1B:40
  i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
  j) c= BDD C implies i+1 < len Gauge(C,n);

theorem :: JORDAN1B:41
  (ex i,j st i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,
  n),i,j) c= BDD C) implies n >= 1;