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

begin

theorem :: JORDAN1I:1

canceled;

theorem :: JORDAN1I:2

canceled;

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 (W-min (L~ (Cage C,n))) .. (Cage C,n) > 1

proof end;

theorem Th4: :: JORDAN1I:4

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

proof end;

theorem Th5: :: JORDAN1I:5

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

proof end;

begin

theorem :: JORDAN1I:6

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

proof end;

theorem Th7: :: JORDAN1I:7

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

proof end;

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 W-min C in right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1

proof end;

theorem :: JORDAN1I:9

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

proof end;

theorem :: JORDAN1I:10

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

proof end;

begin

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 `1 < W-bound (L~ f) holds
p in LeftComp f

proof end;

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 `1 > E-bound (L~ f) holds
p in LeftComp f

proof end;

theorem Th13: :: JORDAN1I:13

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

proof end;

theorem Th14: :: JORDAN1I:14

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

proof end;

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 & 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 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 & 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 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 & 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 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 & 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 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 & 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 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 & 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 Th21: :: JORDAN1I:21

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 & 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 Th22: :: JORDAN1I:22

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 & 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 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 & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds
ex i, j being Element of 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: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 & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds
ex i, j being Element of 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 Th25: :: JORDAN1I:25

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 & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Element of 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 Th26: :: JORDAN1I:26

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 & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of 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:27

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

proof end;

theorem :: JORDAN1I:28

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

proof end;

theorem :: JORDAN1I:29

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

proof end;

theorem :: JORDAN1I:30

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 & 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 = sup (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 & j <= width (Gauge C,i) & p = (Gauge C,i) * (Center (Gauge C,i)),j )

proof end;