The abstract of the Mizar article:

Properties of Go-Board --- Part III

by

Jaroslaw Kotowicz, and

Yatsuka Nakamura

Received August 24, 1992

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;