:: 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

theorem Th1: :: JORDAN1I:1

for n being 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

proof end;

theorem Th2: :: JORDAN1I:2

for n being 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

proof end;

theorem Th3: :: JORDAN1I:3

for n being 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

proof end;

theorem :: JORDAN1I:4

for f being V22() 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)

proof end;

theorem Th5: :: JORDAN1I:5

for f being V22() 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)

proof end;

theorem :: JORDAN1I:6

for n being 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)

proof end;

theorem :: JORDAN1I:7

for n being 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)

proof end;

theorem :: JORDAN1I:8

for n being 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)

proof end;

theorem Th9: :: JORDAN1I:9

for f being V22() 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

proof end;

theorem Th10: :: JORDAN1I:10

for f being V22() 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

proof end;

theorem Th11: :: JORDAN1I:11

for f being V22() 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

proof end;

theorem Th12: :: JORDAN1I:12

for f being V22() 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

proof end;

theorem Th13: :: JORDAN1I:13

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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

proof end;

theorem Th14: :: JORDAN1I:14

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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

proof end;

theorem Th15: :: JORDAN1I:15

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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

proof end;

theorem Th16: :: JORDAN1I:16

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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

proof end;

theorem Th17: :: JORDAN1I:17

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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)

proof end;

theorem Th18: :: JORDAN1I:18

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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)

proof end;

theorem Th19: :: JORDAN1I:19

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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)

proof end;

theorem Th20: :: JORDAN1I:20

for f being V22() standard clockwise_oriented special_circular_sequence
for G being Go-board st f is_sequence_on G holds
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)

proof end;

theorem Th21: :: JORDAN1I:21

for f being V22() standard clockwise_oriented 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) holds
ex i, j being 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)) )

proof end;

theorem :: JORDAN1I:22

for f being V22() standard clockwise_oriented 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) holds
ex i, j being 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) )

proof end;

theorem Th23: :: JORDAN1I:23

for f being V22() standard clockwise_oriented 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) holds
ex i, j being 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) )

proof end;

theorem Th24: :: JORDAN1I:24

for f being V22() standard clockwise_oriented 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) holds
ex i, j being 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) )

proof end;

theorem :: JORDAN1I:25

for f being V22() standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) )

proof end;

theorem :: JORDAN1I:26

for f being V22() standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) )

proof end;

theorem :: JORDAN1I:27

for f being V22() standard special_circular_sequence holds
( f is clockwise_oriented iff (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) )

proof end;

theorem :: JORDAN1I:28

for i, k being 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 & 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)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )

proof end;