:: Introduction to Go-Board - Part II. :: Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$ :: 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, REAL_1, SUBSET_1, GOBOARD1, NAT_1, XBOOLE_0, CARD_1, ARYTM_3, XXREAL_0, TARSKI, ARYTM_1, RELAT_1, ORDINAL4, PARTFUN1, FUNCT_1, RLTOPSP1, TOPREAL1, MCART_1, MATRIX_1, INCSP_1, ZFMISC_1, TREES_1, ORDINAL2, COMPLEX1, STRUCT_0, GOBOARD2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, SEQ_4, MATRIX_0, MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0; constructors PARTFUN1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, TOPREAL1, GOBOARD1, XXREAL_2, SEQM_3, RELSET_1, DOMAIN_1, BINOP_2, RVSUM_1, REAL_1; registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, VALUED_0, CARD_1, SEQM_3, SEQ_4, INT_1, ORDINAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve p,p1,p2,q for Point of TOP-REAL 2, f,f1,f2,g,g1,g2 for FinSequence of TOP-REAL 2, r,s for Real, n,m,i,j,k for Nat, G for Go-board, x for set; theorem :: GOBOARD2:1 (for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in dom f holds LSeg(f,n) misses LSeg(f,m)) implies f is s.n.c.; theorem :: GOBOARD2:2 f is unfolded s.n.c. one-to-one & f/.len f in LSeg(f,i) & i in dom f & i+1 in dom f implies i+1=len f; theorem :: GOBOARD2:3 k<>0 & len f = k+1 implies L~f = L~(f|k) \/ LSeg(f,k); theorem :: GOBOARD2:4 1 < k & len f = k+1 & f is unfolded s.n.c. implies L~(f|k) /\ LSeg(f,k ) = {f/.k}; theorem :: GOBOARD2:5 len f1 < n & n+1 <= len (f1^f2) & m+len f1 = n implies LSeg(f1^f2,n) = LSeg(f2,m); theorem :: GOBOARD2:6 L~f c= L~(f^g); theorem :: GOBOARD2:7 f is s.n.c. implies f|i is s.n.c.; theorem :: GOBOARD2:8 f1 is special & f2 is special & ((f1/.len f1)`1=(f2/.1)`1 or (f1/.len f1)`2=(f2/.1)`2) implies f1^f2 is special; theorem :: GOBOARD2:9 f <> {} implies X_axis(f) <> {}; theorem :: GOBOARD2:10 f <> {} implies Y_axis(f) <> {}; registration let f be non empty FinSequence of TOP-REAL 2; cluster X_axis f -> non empty; cluster Y_axis f -> non empty; end; theorem :: GOBOARD2:11 f is special implies for n being Nat st n in dom f & n+1 in dom f for i,j,m,k being Nat st [i,j] in Indices G & [m,k] in Indices G & f/.n=G*(i,j) & f/.(n+1 )=G*(m,k) holds i=m or k=j; theorem :: GOBOARD2:12 (for n being Nat st n in dom f ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)) & f is special & (for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1)) implies ex g st g is_sequence_on G & L~f = L~g & g/.1=f/.1 & g/.len g=f/.len f & len f<=len g; definition let v1,v2 be FinSequence of REAL; assume v1 <> {}; func GoB(v1,v2) -> Matrix of TOP-REAL 2 means :: GOBOARD2:def 1 len it = len v1 & width it = len v2 & for n,m being Nat st [n,m] in Indices it holds it*(n,m) = |[v1.n,v2.m]|; end; registration let v1,v2 be non empty FinSequence of REAL; cluster GoB(v1,v2) -> non empty-yielding X_equal-in-line Y_equal-in-column; end; registration let v1,v2 be non empty increasing FinSequence of REAL; cluster GoB(v1,v2) -> Y_increasing-in-line X_increasing-in-column; end; definition let f be non empty FinSequence of TOP-REAL 2; func GoB(f) -> Matrix of TOP-REAL 2 equals :: GOBOARD2:def 2 GoB(Incr(X_axis(f)),Incr(Y_axis(f))); end; registration let f be non empty FinSequence of TOP-REAL 2; cluster GoB(f) -> non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column; end; reserve f for non empty FinSequence of TOP-REAL 2; theorem :: GOBOARD2:13 len GoB(f) = card rng X_axis(f) & width GoB(f) = card rng Y_axis (f); theorem :: GOBOARD2:14 for n st n in dom f holds ex i,j st [i,j] in Indices GoB(f) & f/.n = GoB(f)*(i,j); theorem :: GOBOARD2:15 n in dom f & (for m st m in dom f holds (X_axis(f)).n <= (X_axis(f)).m ) implies f/.n in rng Line(GoB(f),1); theorem :: GOBOARD2:16 n in dom f & (for m st m in dom f holds (X_axis(f)).m <= (X_axis(f)).n ) implies f/.n in rng Line(GoB(f),len GoB(f)); theorem :: GOBOARD2:17 n in dom f & (for m st m in dom f holds (Y_axis(f)).n <= (Y_axis(f)).m ) implies f/.n in rng Col(GoB(f),1); theorem :: GOBOARD2:18 n in dom f & (for m st m in dom f holds (Y_axis(f)).m <= (Y_axis(f)).n ) implies f/.n in rng Col(GoB(f),width GoB(f));