:: On the General Position of Special Polygons
::  by Mariusz Giero
::
:: Received May 27, 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, REAL_1, FINSEQ_1, RELAT_1, ZFMISC_1, XBOOLE_0,
      ARYTM_3, CARD_1, ARYTM_1, ABIAN, EUCLID, XXREAL_0, PARTFUN1, FUNCT_1,
      TOPREAL1, GOBOARD5, NAT_1, RLTOPSP1, GRAPH_2, TARSKI, STRUCT_0, PRE_TOPC,
      SETFAM_1, FINSET_1, CONNSP_1, GOBOARD9, GOBOARD1, MCART_1, CONVEX1,
      TREES_1, GOBOARD2, FINSEQ_5, SPPOL_1, MATRIX_1, TOPS_1, INT_1, JORDAN12;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1,
      NUMBERS, XCMPLX_0, XREAL_0, INT_1, NAT_1, NAT_D, ABIAN, GRAPH_2,
      FINSET_1, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, STRUCT_0, PRE_TOPC,
      TOPS_1, CONNSP_1, RLTOPSP1, EUCLID, TOPREAL1, SPPOL_1, GOBOARD1,
      GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, XXREAL_0, FINSEQ_6;
 constructors SETFAM_1, NAT_D, ABIAN, TOPS_1, CONNSP_1, GOBOARD2, SPPOL_1,
      GRAPH_2, GOBOARD9, GOBRD13, XXREAL_2, RELSET_1, CONVEX1, FINSEQ_6;
 registrations SUBSET_1, XREAL_0, INT_1, MEMBERED, ABIAN, GOBOARD2, SPPOL_2,
      GOBOARD5, GOBOARD9, RELAT_1, ZFMISC_1, EUCLID, FINSET_1, FINSEQ_1,
      JORDAN1, RLTOPSP1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

reserve i,j,k,n for Nat,
  X,Y,a,b,c,x for set,
  r,s for Real;

theorem :: JORDAN12:1
  1 < i implies 0 < i-'1;

theorem :: JORDAN12:2
  1 is odd;

theorem :: JORDAN12:3
  for f be FinSequence of TOP-REAL n for i st 1 <= i & i + 1 <= len
  f holds f/.i in rng f & f/.(i+1) in rng f;

registration
  cluster s.n.c. -> s.c.c. for FinSequence of TOP-REAL 2;
end;

theorem :: JORDAN12:4
  for f,g be FinSequence of TOP-REAL 2 st f ^' g is unfolded s.c.c.
  & len g >= 2 holds f is unfolded s.n.c.;

theorem :: JORDAN12:5
  for g1,g2 be FinSequence of TOP-REAL 2 holds L~g1 c= L~(g1^'g2);

begin

definition
  let n;
  let f1,f2 be FinSequence of TOP-REAL n;
  pred f1 is_in_general_position_wrt f2 means
:: JORDAN12:def 1

  L~f1 misses rng f2 & for
  i st 1<=i & i < len f2 holds L~f1 /\ LSeg(f2,i) is trivial;
end;

definition
  let n;
  let f1,f2 be FinSequence of TOP-REAL n;
  pred f1,f2 are_in_general_position means
:: JORDAN12:def 2

  f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1;
  symmetry;
end;

theorem :: JORDAN12:6
  for f1,f2 being FinSequence of TOP-REAL 2
   st f1,f2 are_in_general_position
  for f being FinSequence of TOP-REAL 2
   st f = f2|(Seg k) holds f1,f are_in_general_position;

theorem :: JORDAN12:7
  for f1,f2,g1,g2 be FinSequence of TOP-REAL 2 st f1^'f2,g1^'g2
  are_in_general_position holds f1^'f2,g1 are_in_general_position;

reserve f,g for FinSequence of TOP-REAL 2;

theorem :: JORDAN12:8
  for k,f,g st 1<=k & k+1<=len g & f,g are_in_general_position
  holds g.k in (L~f)` & g.(k+1) in (L~f)`;

theorem :: JORDAN12:9
  for f1,f2 be FinSequence of TOP-REAL 2 st f1,f2
are_in_general_position for i,j st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <=
  len f2 holds LSeg(f1,i) /\ LSeg(f2,j) is trivial;

theorem :: JORDAN12:10
  for f,g holds
  INTERSECTION({ LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f }
  , { LSeg(g,j) where j is Nat : 1 <= j & j+1 <= len g }) is finite;

theorem :: JORDAN12:11
  for f,g st f,g are_in_general_position holds L~f /\ L~g is finite;

theorem :: JORDAN12:12
  for f,g st f,g are_in_general_position for k holds L~f /\ LSeg(g
  ,k) is finite;

begin

reserve f for non constant standard special_circular_sequence,
  p,p1,p2,q for Point of TOP-REAL 2;

theorem :: JORDAN12:13
  for f,p1,p2 st LSeg(p1,p2) misses L~f holds ex C be Subset of
  TOP-REAL 2 st C is_a_component_of (L~f)` & p1 in C & p2 in C;

theorem :: JORDAN12:14
  (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a
in C & b in C)) iff ( a in RightComp f & b in RightComp f or a in LeftComp f &
  b in LeftComp f );

theorem :: JORDAN12:15
  a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
  (C is_a_component_of (L~f)` & a in C & b in C)) iff ( a in LeftComp f & b in
  RightComp f or a in RightComp f & b in LeftComp f );

theorem :: JORDAN12:16
  for f,a,b,c st (ex C be Subset of TOP-REAL 2 st (C
is_a_component_of (L~f)` & a in C & b in C)) & (ex C be Subset of TOP-REAL 2 st
  (C is_a_component_of (L~f)` & b in C & c in C)) holds ex C be Subset of
  TOP-REAL 2 st C is_a_component_of (L~f)` & a in C & c in C;

theorem :: JORDAN12:17
  for f,a,b,c st a in (L~f)` & b in (L~f)` & c in (L~f)` & (not ex
C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a in C & b in C)) &
  (not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & b in C & c
in C)) holds ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & a in
  C & c in C;

begin

reserve G for Go-board;

theorem :: JORDAN12:18
  i <= len G implies v_strip(G,i) is convex;

theorem :: JORDAN12:19
  j <= width G implies h_strip(G,j) is convex;

theorem :: JORDAN12:20
  i <= len G & j <= width G implies cell(G,i,j) is convex;

theorem :: JORDAN12:21
  for f,k st 1<=k & k+1<=len f holds left_cell(f,k) is convex;

theorem :: JORDAN12:22
  for f,k st 1<=k & k+1<=len f holds left_cell(f,k,GoB f) is
  convex & right_cell(f,k,GoB f) is convex;

begin

theorem :: JORDAN12:23
  for p1,p2,f for r be Point of TOP-REAL 2 st r in LSeg(p1,p2) & (
ex x st (L~f) /\ LSeg(p1,p2) = {x}) & not r in L~f holds L~f misses LSeg(p1,r)
  or L~f misses LSeg(r,p2);

theorem :: JORDAN12:24
  for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is vertical &
  LSeg(r,s) is vertical & LSeg(p,q) meets LSeg(r,s) holds p`1 = r`1;

theorem :: JORDAN12:25
  for p,p1,p2 st not p in LSeg(p1,p2) & p1`2 = p2`2 & p2`2 = p`2
  holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);

theorem :: JORDAN12:26
  for p,p1,p2 st not p in LSeg(p1,p2) & p1`1 = p2`1 & p2`1 = p`1
  holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);

theorem :: JORDAN12:27
  p <> p1 & p <> p2 & p in LSeg(p1,p2) implies not p1 in LSeg(p,p2 );

theorem :: JORDAN12:28
  for p,p1,p2,q st not q in LSeg(p1,p2) & p in LSeg(p1,p2) & p <>
p1 & p <> p2 & (p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2) holds p1
  in LSeg(q,p) or p2 in LSeg(q,p);

theorem :: JORDAN12:29
  for p1,p2,p3,p4,p be Point of TOP-REAL 2 st (p1`1 = p2`1 & p3`1
= p4`1 or p1`2 = p2`2 & p3`2 = p4`2) & LSeg(p1,p2) /\ LSeg(p3,p4) = {p} holds p
  =p1 or p=p2 or p=p3;

begin

theorem :: JORDAN12:30
  for p,p1,p2,f st (L~f) /\ LSeg(p1,p2) = {p} for r be Point of
  TOP-REAL 2 st not r in LSeg(p1,p2) & not p1 in L~f & not p2 in L~f & ( p1`1 =
p2`1 & p1`1 = r`1 or p1`2 = p2`2 & p1`2 = r`2 ) & (ex i st (1<=i & i+1<= len f
& (r in right_cell(f,i,GoB f) or r in left_cell(f,i,GoB f)) & p in LSeg(f,i)))
& not r in L~f holds (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f
)` & r in C & p1 in C)) or ex C be Subset of TOP-REAL 2 st C is_a_component_of
  (L~f)` & r in C & p2 in C;

theorem :: JORDAN12:31
  for f,p1,p2,p st (L~f) /\ LSeg(p1,p2) = {p} for rl,rp be Point
of TOP-REAL 2 st not p1 in L~f & not p2 in L~f & ( p1`1 = p2`1 & p1`1 = rl`1 &
rl`1 = rp`1 or p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2 ) & (ex i st (1<=i & i+1
<= len f & rl in left_cell(f,i,GoB f) & rp in right_cell(f,i,GoB f) & p in LSeg
(f,i))) & not rl in L~f & not rp in L~f holds not ex C be Subset of TOP-REAL 2
  st (C is_a_component_of (L~f)` & p1 in C & p2 in C);

theorem :: JORDAN12:32
  for p,f,p1,p2 st L~f /\ LSeg(p1,p2) = {p} & (p1`1=p2`1 or p1`2=
p2`2) & not p1 in L~f & not p2 in L~f & rng f misses LSeg(p1,p2) holds not ex C
  be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & p1 in C & p2 in C);

theorem :: JORDAN12:33
  for f being non constant standard special_circular_sequence, g
being special FinSequence of TOP-REAL 2 st f,g are_in_general_position for k st
1<=k & k+1<= len g holds card (L~f /\ LSeg(g,k)) is even Element of NAT iff ex
C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & g.k in C & g.(k+1) in
  C;

theorem :: JORDAN12:34
  for f1,f2,g1 being special FinSequence of TOP-REAL 2 st f1 ^' f2
  is non constant standard special_circular_sequence & f1 ^' f2, g1
are_in_general_position & len g1 >= 2 & g1 is unfolded s.n.c. holds card (L~(f1
  ^' f2) /\ L~g1) is even Element of NAT iff ex C be Subset of TOP-REAL 2 st C
  is_a_component_of (L~(f1 ^' f2))` & g1.1 in C & g1.len g1 in C;

theorem :: JORDAN12:35
  for f1,f2,g1,g2 being special FinSequence of TOP-REAL 2 st f1 ^' f2 is
  non constant standard special_circular_sequence & g1 ^' g2 is non constant
  standard special_circular_sequence & L~f1 misses L~g2 & L~f2 misses L~g1 & f1
^' f2, g1 ^' g2 are_in_general_position for p1,p2,q1,q2 being Point of TOP-REAL
2 st f1.1 = p1 & f1.len f1 = p2 & g1.1 = q1 & g1.len g1 = q2 & f1/.len f1 = f2
  /.1 & g1/.len g1 = g2/.1 & p1 in L~f1 /\ L~f2 & q1 in L~g1 /\ L~g2 & ex C be
Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))` & q1 in C & q2 in C
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(g1 ^' g2))` & p1 in C &
  p2 in C;