JORDAN1I: Some Remarks on Clockwise Oriented Sequences on Go-boards

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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, PSCOMP_1, TOPREAL1, JORDAN9, FINSEQ_4, XXREAL_0, PARTFUN1, ARYTM_3, FUNCT_1, GOBOARD5, PRE_TOPC, RELAT_1, FINSEQ_6, FINSEQ_1, MATRIX_1, GOBOARD2, ARYTM_1, XBOOLE_0, JORDAN8, TREES_1, GOBOARD1, MCART_1, COMPLEX1, CARD_1, RLTOPSP1, TARSKI, SPRECT_2, GOBOARD9, JORDAN2C, TOPS_1, REAL_1, JORDAN5D, CONNSP_1, TOPREAL2, JORDAN1A, JORDAN6, JORDAN1E, SEQ_4, XXREAL_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, FUNCT_1, NAT_D, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, FINSEQ_6, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, TOPREAL2, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN5D, JORDAN1A, JORDAN1E, XXREAL_0;
definitions TARSKI;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5, JORDAN4, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, GOBOARD9, SPPOL_2, REVROT_1, TOPREAL1, GOBRD13, JORDAN9, JORDAN2C, ABSVALUE, GOBOARD1, TARSKI, TOPREAL3, FINSEQ_3, UNIFORM1, FUNCT_1, JORDAN1B, SPRECT_5, JORDAN5D, JORDAN1E, JORDAN1F, JORDAN1G, JORDAN1H, TOPREAL8, GOBRD14, JORDAN1D, GOBOARD6, SPRECT_1, XBOOLE_0, XBOOLE_1, XREAL_1, JORDAN6, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3;
schemes ;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, GOBOARD2, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, FUNCT_1, EUCLID, JORDAN2C, XREAL_0, NAT_1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, TOPS_1, CONNSP_1, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN6, JORDAN5D, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1;
expansions ;

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

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

proof end;

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

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 `2 > N-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 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 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 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

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

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 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 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 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 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 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 non constant 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 non constant 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 non constant 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 non constant 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 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: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) )

proof end;

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

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;