:: Some Remarks on Clockwise Oriented Sequences on Go-boards
:: by Adam Naumowicz and Robert Milewski
::
:: Received March 1, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

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

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

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

begin

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

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

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

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

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

begin

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th21: :: JORDAN1I:21
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G &amp; 1 <= k &amp; k + 1 <= len f &amp; f /. k = W-min (L~ f) holds
ex i, j being Element of NAT st
( [i,j] in Indices G &amp; [i,(j + 1)] in Indices G &amp; f /. k = G * (i,j) &amp; f /. (k + 1) = G * (i,(j + 1)) )
proofend;

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

theorem Th23: :: JORDAN1I:23
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G &amp; 1 <= k &amp; k + 1 <= len f &amp; f /. k = E-max (L~ f) holds
ex i, j being Element of NAT st
( [i,(j + 1)] in Indices G &amp; [i,j] in Indices G &amp; f /. k = G * (i,(j + 1)) &amp; f /. (k + 1) = G * (i,j) )
proofend;

theorem Th24: :: JORDAN1I:24
for f being non constant standard clockwise_oriented special_circular_sequence
for G being Go-board
for k being Element of NAT st f is_sequence_on G &amp; 1 <= k &amp; k + 1 <= len f &amp; f /. k = S-max (L~ f) holds
ex i, j being Element of NAT st
( [(i + 1),j] in Indices G &amp; [i,j] in Indices G &amp; f /. k = G * ((i + 1),j) &amp; f /. (k + 1) = G * (i,j) )
proofend;

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) )
proofend;

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) )
proofend;

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) )
proofend;

theorem :: JORDAN1I:28
for i, k being Element of NAT
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 &amp; i > 0 &amp; 1 <= k &amp; k <= width (Gauge (C,i)) &amp; (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) &amp; 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)))))) holds
ex j being Element of NAT st
( 1 <= j &amp; j <= width (Gauge (C,i)) &amp; p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
proofend;