:: Properties of Go-Board - Part III :: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura :: :: Received August 24, 1992 :: Copyright (c) 1992-2021 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, PRE_TOPC, EUCLID, FINSEQ_1, SUBSET_1, GOBOARD1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0, TOPREAL1, NAT_1, RLTOPSP1, PARTFUN1, MATRIX_1, FUNCT_1, COMPLEX1, ARYTM_1, ZFMISC_1, TREES_1, INCSP_1, TARSKI, XBOOLE_0, ORDINAL2, MCART_1, ORDINAL4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, FUNCT_1, PARTFUN1, SEQM_3, FINSEQ_1, PRE_TOPC, MATRIX_0, STRUCT_0, MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0; constructors COMPLEX1, TOPREAL1, GOBOARD1, RELSET_1, DOMAIN_1, MATRIX_1, REAL_1; registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, EUCLID, INT_1, CARD_1, FINSEQ_1, VALUED_0; 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 being_S-Seq implies ex g st g is_sequence_on G & g is being_S-Seq & L~f = L~ g & f/.1 = g/.1 & f/.len f = g/.len g & len f<=len g;