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

### Properties of Go-Board --- Part III

by
Jaroslaw Kotowicz, and
Yatsuka Nakamura

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

```environ

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

begin

reserve p,p1,p2,q for Point of TOP-REAL 2,
f,g,g1,g2 for FinSequence of TOP-REAL 2,
n,m,i,j,k for Nat,
G for Go-board,
x for set;

theorem :: GOBOARD3:1
(for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) &
f is one-to-one unfolded s.n.c. special
implies
ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special &
L~f = L~g & f/.1 = g/.1 & f/.len f = g/.len g & len f <= len g;

theorem :: GOBOARD3:2
(for n st n in dom f ex i,j st [i,j] in Indices G &
f/.n=G*(i,j)) & f is_S-Seq implies
ex g st g is_sequence_on G & g is_S-Seq & L~f = L~g & f/.1 = g/.1 &
f/.len f = g/.len g & len f<=len g;
```