Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Go-Board Theorem

by
Jaroslaw Kotowicz, and
Yatsuka Nakamura

MML identifier: GOBOARD4
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, EUCLID, FINSEQ_1, GOBOARD1, FINSEQ_4, RELAT_1, INCSP_1,
MATRIX_1, TREES_1, BOOLE, FUNCT_1, ARYTM_1, ABSVALUE, MATRIX_2, TOPREAL1,
GOBOARD2, MCART_1, TOPREAL4, GOBOARD4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
NAT_1, FUNCT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, ABSVALUE, FINSEQ_4,
MATRIX_1, EUCLID, TOPREAL1, TOPREAL4, GOBOARD1, GOBOARD2;
constructors REAL_1, NAT_1, ABSVALUE, TOPREAL1, MATRIX_2, TOPREAL4, GOBOARD2,
FINSEQ_4, INT_1, MEMBERED, XBOOLE_0;
clusters GOBOARD1, RELSET_1, GOBOARD2, STRUCT_0, EUCLID, INT_1, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2,
P1,P2 for Subset of TOP-REAL 2,
f,f1,f2,g1,g2 for FinSequence of TOP-REAL 2,
n,m,i,j,k for Nat,
G,G1 for Go-board,
x,y for set;

theorem :: GOBOARD4:1
for G,f1,f2 st 1<=len f1 & 1<=len f2 &
f1 is_sequence_on G & f2 is_sequence_on G &
f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
rng f1 meets rng f2;

theorem :: GOBOARD4:2
for G,f1,f2 st 2<=len f1 & 2<=len f2 &
f1 is_sequence_on G & f2 is_sequence_on G &
f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
L~f1 meets L~f2;

theorem :: GOBOARD4:3
for G,f1,f2 st 2 <= len f1 & 2 <= len f2 &
f1 is_sequence_on G & f2 is_sequence_on G &
f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
L~f1 meets L~f2;

definition let f be FinSequence of REAL, r,s be Real;
pred f lies_between r,s means
:: GOBOARD4:def 1
for n st n in dom f holds r <= f.n & f.n <= s;
end;

definition let D be non empty set;
let f1 be FinSequence of D, f2 be non empty FinSequence of D;
cluster f1^f2 -> non empty;
cluster f2^f1 -> non empty;
end;

theorem :: GOBOARD4:4
for f1,f2 being FinSequence of TOP-REAL 2 st
2<=len f1 & 2<=len f2 & f1 is special & f2 is special &
(for n st n in dom f1 & n+1 in dom f1 holds f1/.n <> f1/.(n+1)) &
(for n st n in dom f2 & n+1 in dom f2 holds f2/.n <> f2/.(n+1)) &
X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
L~f1 meets L~f2;

theorem :: GOBOARD4:5
for f1,f2 being FinSequence of TOP-REAL 2 st
f1 is one-to-one special & 2 <= len f1 &
f2 is one-to-one special & 2 <= len f2 &
X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
L~f1 meets L~f2;

canceled 2;

theorem :: GOBOARD4:8
for P1,P2,p1,p2,q1,q2 st
P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 &
(for p st p in P1 \/ P2 holds p1`1<=p`1 & p`1<=q1`1) &
(for p st p in P1 \/ P2 holds p2`2<=p`2 & p`2<=q2`2) holds
P1 meets P2;
```