:: Some Remarks on Clockwise Oriented Sequences on Go-boards
:: by Adam Naumowicz and Robert Milewski
::
:: Received March 1, 2002
:: Copyright (c) 2002-2017 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, 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 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;
constructors 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;
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;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Preliminaries
reserve i,j,k,n for Nat;
theorem :: JORDAN1I:1
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (W-min L~Cage(C,n))..Cage(C,n) > 1;
theorem :: JORDAN1I:2
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (E-max L~Cage(C,n))..Cage(C,n) > 1;
theorem :: JORDAN1I:3
for C being compact connected non vertical non horizontal Subset
of TOP-REAL 2 holds (S-max L~Cage(C,n))..Cage(C,n) > 1;
begin :: On bounding points of circular sequences
theorem :: JORDAN1I:4
for f being non constant standard special_circular_sequence, p being
Point of TOP-REAL 2 st p in rng f holds left_cell(f,p..f) = left_cell(Rotate(f,
p),1);
theorem :: JORDAN1I:5
for f being non constant standard special_circular_sequence, p
being Point of TOP-REAL 2 st p in rng f holds right_cell(f,p..f) = right_cell(
Rotate(f,p),1);
theorem :: JORDAN1I:6
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds W-min C in right_cell(Rotate(Cage(C,n),W-min L~Cage(
C,n)),1);
theorem :: JORDAN1I:7
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds E-max C in right_cell(Rotate(Cage(C,n),E-max L~Cage(
C,n)),1);
theorem :: JORDAN1I:8
for C being compact connected non vertical non horizontal non empty
Subset of TOP-REAL 2 holds S-max C in right_cell(Rotate(Cage(C,n),S-max L~Cage(
C,n)),1);
begin :: On clockwise oriented sequences
theorem :: JORDAN1I:9
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`1 < W-bound (L~f
) holds p in LeftComp f;
theorem :: JORDAN1I:10
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`1 > E-bound (L~f
) holds p in LeftComp f;
theorem :: JORDAN1I:11
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`2 < S-bound (L~f
) holds p in LeftComp f;
theorem :: JORDAN1I:12
for f being clockwise_oriented non constant standard
special_circular_sequence for p being Point of TOP-REAL 2 st p`2 > N-bound (L~f
) holds p in LeftComp f;
theorem :: JORDAN1I:13
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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;
theorem :: JORDAN1I:14
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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;
theorem :: JORDAN1I:15
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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;
theorem :: JORDAN1I:16
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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;
theorem :: JORDAN1I:17
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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
;
theorem :: JORDAN1I:18
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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
;
theorem :: JORDAN1I:19
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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
;
theorem :: JORDAN1I:20
for f being clockwise_oriented non constant standard
special_circular_sequence for G being Go-board st f is_sequence_on G 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
;
theorem :: JORDAN1I:21
for f being clockwise_oriented non constant standard
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
ex i,j be 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);
theorem :: JORDAN1I:22
for f being clockwise_oriented non constant standard
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
ex i,j be 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);
theorem :: JORDAN1I:23
for f being clockwise_oriented non constant standard
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
ex i,j be 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);
theorem :: JORDAN1I:24
for f being clockwise_oriented non constant standard
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
ex i,j be 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);
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;
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;
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;
theorem :: JORDAN1I:28
for C being compact non vertical non horizontal non empty
being_simple_closed_curve Subset of TOP-REAL 2 for p being Point of TOP-REAL 2
holds 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))) implies ex j st 1 <= j & j <= width Gauge(C,i) & p =
Gauge(C,i)*(Center Gauge(C,i),j);