Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Introduction to Go-Board --- Part I

**by****Jaroslaw Kotowicz, and****Yatsuka Nakamura**- Received August 24, 1992
- MML identifier: GOBOARD1

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, EUCLID, FINSEQ_1, ABSVALUE, ARYTM_1, FINSEQ_4, FUNCT_1, RELAT_1, BOOLE, FINSET_1, CARD_1, FINSEQ_2, MATRIX_2, ORDINAL2, SEQM_3, MCART_1, TOPREAL1, MATRIX_1, TREES_1, INCSP_1, GOBOARD1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, CARD_1, FINSEQ_1, FINSET_1, SEQM_3, STRUCT_0, PRE_TOPC, ABSVALUE, FINSEQ_2, FINSEQ_4, EUCLID, TOPREAL1, MATRIX_1, MATRIX_2; constructors REAL_1, NAT_1, SEQM_3, ABSVALUE, TOPREAL1, MATRIX_2, FINSEQ_4, INT_1, MEMBERED, PARTFUN1, XBOOLE_0; clusters FINSET_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1, RELAT_1, TOPREAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve p for Point of TOP-REAL 2, f,f1,f2,g for FinSequence of TOP-REAL 2, v,v1,v2 for FinSequence of REAL, r,s for Real, n,m,i,j,k for Nat, x for set; ::::::::::::::::::::::::::::: :: Real numbers preliminaries ::::::::::::::::::::::::::::: theorem :: GOBOARD1:1 abs(r-s)=1 iff r>s & r=s+1 or r<s & s=r+1; theorem :: GOBOARD1:2 abs(i-j)+abs(n-m)=1 iff abs(i-j)=1 & n=m or abs(n-m)=1 & i=j; theorem :: GOBOARD1:3 n>1 iff ex m st n=m+1 & m>0; begin :: Finite sequences preliminaries scheme FinSeqDChoice{D()->non empty set, N()->Nat, P[set,set]}: ex f being FinSequence of D() st len f = N() & for n st n in Seg N() holds P[n,f/.n] provided for n st n in Seg N() ex d being Element of D() st P[n,d]; theorem :: GOBOARD1:4 n = m + 1 & i in Seg n implies len Sgm(Seg n \ {i}) = m; theorem :: GOBOARD1:5 n=m+1 & k in Seg n & i in Seg m implies (1<=i & i<k implies Sgm(Seg n \ {k}).i = i) & (k<=i & i<=m implies Sgm(Seg n \ {k}).i = i+1); theorem :: GOBOARD1:6 for f being FinSequence, n,m st len f = m+1 & n in dom f holds len Del(f,n)=m; theorem :: GOBOARD1:7 for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in Seg m holds Del(f,n).k = f.k or Del(f,n).k = f.(k+1); theorem :: GOBOARD1:8 for f being FinSequence,n,m,k st len f = m+1 & k<n holds Del(f,n).k = f.k; theorem :: GOBOARD1:9 for f being FinSequence,n,m,k st len f = m+1 & n in dom f & n<=k & k<=m holds Del(f,n).k = f.(k+1); theorem :: GOBOARD1:10 for D being set, f being FinSequence of D, n,m st n in dom f & m in Seg n holds m in dom f & (f|n)/.m = f/.m; definition let f be FinSequence of REAL, k be Nat; redefine func f.k -> Real; end; definition let IT be FinSequence of REAL; attr IT is increasing means :: GOBOARD1:def 1 for n,m st n in dom IT & m in dom IT & n<m holds IT.n < IT.m; end; definition let f be FinSequence; redefine attr f is constant means :: GOBOARD1:def 2 for n,m st n in dom f & m in dom f holds f.n=f.m; end; definition cluster non empty increasing FinSequence of REAL; end; definition let D be non empty set; cluster non empty FinSequence of D; end; definition cluster constant FinSequence of REAL; end; definition let f; func X_axis(f) -> FinSequence of REAL means :: GOBOARD1:def 3 len it = len f & for n st n in dom it holds it.n = (f/.n)`1; func Y_axis(f) -> FinSequence of REAL means :: GOBOARD1:def 4 len it = len f & for n st n in dom it holds it.n = (f/.n)`2; end; canceled 3; theorem :: GOBOARD1:14 v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) & i in Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i holds k<=m) implies m+1 in dom v & v.(m+1)=i+1; theorem :: GOBOARD1:15 v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m<k & k in dom v & r = v.k holds i<r; theorem :: GOBOARD1:16 i in dom f & 2<=len f implies f/.i in L~f; begin ::::::::::::::::::::::: :: Matrix preliminaries ::::::::::::::::::::::: theorem :: GOBOARD1:17 for D being non empty set,M being Matrix of D holds for i,j st j in dom M & i in Seg width M holds Col(M,i).j = Line(M,j).i; definition let D be non empty set; let M be Matrix of D; redefine attr M is empty-yielding means :: GOBOARD1:def 5 0 = len M or 0 = width M; end; definition let M be Matrix of TOP-REAL 2; attr M is X_equal-in-line means :: GOBOARD1:def 6 for n st n in dom M holds X_axis(Line(M,n)) is constant; attr M is Y_equal-in-column means :: GOBOARD1:def 7 for n st n in Seg width M holds Y_axis(Col(M,n)) is constant; attr M is Y_increasing-in-line means :: GOBOARD1:def 8 for n st n in dom M holds Y_axis(Line(M,n)) is increasing; attr M is X_increasing-in-column means :: GOBOARD1:def 9 for n st n in Seg width M holds X_axis(Col(M,n)) is increasing; end; definition cluster non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of TOP-REAL 2; end; canceled; theorem :: GOBOARD1:19 for M being X_increasing-in-column X_equal-in-line Matrix of TOP-REAL 2 holds for x,n,m st x in rng Line(M,n) & x in rng Line(M,m) & n in dom M & m in dom M holds n=m; theorem :: GOBOARD1:20 for M being Y_increasing-in-line Y_equal-in-column Matrix of TOP-REAL 2 holds for x,n,m st x in rng Col(M,n) & x in rng Col(M,m) & n in Seg width M & m in Seg width M holds n=m; begin ::::::::::::::::::::: :: Go board ::::::::::::::::::::: definition mode Go-board is non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of TOP-REAL 2; end; reserve G for Go-board; theorem :: GOBOARD1:21 x=G*(m,k) & x=G*(i,j) & [m,k] in Indices G & [i,j] in Indices G implies m=i & k=j; theorem :: GOBOARD1:22 m in dom f & f/.1 in rng Col(G,1) implies (f|m)/.1 in rng Col(G,1); theorem :: GOBOARD1:23 m in dom f & f/.m in rng Col(G,width G) implies (f|m)/.len(f|m) in rng Col(G,width G); theorem :: GOBOARD1:24 rng f misses rng Col(G,i) & f/.n = G*(m,k) & n in dom f & m in dom G implies i<>k; definition let G,i; assume i in Seg width G & width G > 1; func DelCol(G,i) -> Go-board means :: GOBOARD1:def 10 len it = len G & for k st k in dom G holds it.k = Del(Line(G,k),i); end; theorem :: GOBOARD1:25 i in Seg width G & width G > 1 & k in dom G implies Line(DelCol(G,i),k) = Del(Line(G,k),i); theorem :: GOBOARD1:26 i in Seg width G & width G = m+1 & m>0 implies width DelCol(G,i) = m; theorem :: GOBOARD1:27 i in Seg width G & width G > 1 implies width G = width DelCol(G,i) + 1; theorem :: GOBOARD1:28 i in Seg width G & width G > 1 & n in dom G & m in Seg width DelCol(G,i) implies DelCol(G,i)*(n,m)=Del(Line(G,n),i).m; theorem :: GOBOARD1:29 i in Seg width G & width G = m+1 & m>0 & 1<=k & k<i implies Col(DelCol(G,i),k) = Col(G,k) & k in Seg width DelCol(G,i) & k in Seg width G; theorem :: GOBOARD1:30 i in Seg width G & width G = m+1 & m>0 & i<=k & k<=m implies Col(DelCol(G,i),k) = Col(G,k+1) & k in Seg width DelCol(G,i) & k+1 in Seg width G; theorem :: GOBOARD1:31 i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k<i implies DelCol(G,i)*(n,k) = G*(n,k) & k in Seg width G; theorem :: GOBOARD1:32 i in Seg width G & width G = m+1 & m>0 & n in dom G & i<=k & k<=m implies DelCol(G,i)*(n,k) = G*(n,k+1) & k+1 in Seg width G; theorem :: GOBOARD1:33 width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,1),k) = Col(G,k+1) & k in Seg width DelCol(G,1) & k+1 in Seg width G; theorem :: GOBOARD1:34 width G = m+1 & m>0 & k in Seg m & n in dom G implies DelCol(G,1)*(n,k) = G*(n,k+1) & 1 in Seg width G; theorem :: GOBOARD1:35 width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,width G),k) = Col(G,k) & k in Seg width DelCol(G,width G); theorem :: GOBOARD1:36 width G = m+1 & m>0 & k in Seg m & n in dom G implies k in Seg width G & DelCol(G,width G)*(n,k) = G*(n,k) & width G in Seg width G; theorem :: GOBOARD1:37 rng f misses rng Col(G,i) & f/.n in rng Line(G,m) & n in dom f & i in Seg width G & m in dom G & width G>1 implies f/.n in rng Line(DelCol(G,i),m); reserve D for set, f for FinSequence of D, M for Matrix of D; definition let D,f,M; pred f is_sequence_on M means :: GOBOARD1:def 11 (for n st n in dom f ex i,j st [i,j] in Indices M & f/.n = M*(i,j)) & (for n st n in dom f & n+1 in dom f holds for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & f/.n = M*(m,k) & f/.(n+1) = M*(i,j) holds abs(m-i)+abs(k-j) = 1); end; theorem :: GOBOARD1:38 (m in dom f implies 1 <= len(f|m)) & (f is_sequence_on M implies f|m is_sequence_on M); theorem :: GOBOARD1:39 (for n st n in dom f1 ex i,j st [i,j] in Indices M & f1/.n=M*(i,j)) & (for n st n in dom f2 ex i,j st [i,j] in Indices M & f2/.n=M*(i,j)) implies for n st n in dom(f1^f2) ex i,j st [i,j] in Indices M & (f1^f2)/.n=M*(i,j); theorem :: GOBOARD1:40 (for n st n in dom f1 & n+1 in dom f1 holds for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & f1/.n=M*(m,k) & f1/.(n+1)=M*(i,j) holds abs(m-i)+abs(k-j)=1) & (for n st n in dom f2 & n+1 in dom f2 holds for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & f2/.n=M*(m,k) & f2/.(n+1)=M*(i,j) holds abs(m-i)+abs(k-j)=1) & (for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & f1/.len f1=M*(m,k) & f2/.1=M*(i,j) & len f1 in dom f1 & 1 in dom f2 holds abs(m-i)+abs(k-j)=1) implies for n st n in dom(f1^f2) & n+1 in dom(f1^f2) holds for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & (f1^f2)/.n =M* (m,k) & (f1^f2)/.(n+1)=M*(i,j) holds abs(m-i)+abs(k-j)=1; reserve f for FinSequence of TOP-REAL 2; theorem :: GOBOARD1:41 f is_sequence_on G & i in Seg width G & rng f misses rng Col(G,i) & width G > 1 implies f is_sequence_on DelCol(G,i); theorem :: GOBOARD1:42 f is_sequence_on G & i in dom f implies ex n st n in dom G & f/.i in rng Line(G,n); theorem :: GOBOARD1:43 f is_sequence_on G & i in dom f & i+1 in dom f & n in dom G & f/.i in rng Line(G,n) implies f/.(i+1) in rng Line(G,n) or for k st f/.(i+1) in rng Line(G,k) & k in dom G holds abs(n-k) = 1; theorem :: GOBOARD1:44 1<=len f & f/.len f in rng Line(G,len G) & f is_sequence_on G & i in dom G & i+1 in dom G & m in dom f & f/.m in rng Line(G,i) & (for k st k in dom f & f/.k in rng Line(G,i) holds k<=m) implies m+1 in dom f & f/.(m+1) in rng Line(G,i+1); theorem :: GOBOARD1:45 1<=len f & f/.1 in rng Line(G,1) & f/.len f in rng Line(G,len G) & f is_sequence_on G implies (for i st 1<=i & i<=len G holds ex k st k in dom f & f/.k in rng Line(G,i)) & (for i st 1<=i & i<=len G & 2<=len f holds L~f meets rng Line(G,i)) & for i,j,k,m st 1<=i & i<=len G & 1<=j & j<=len G & k in dom f & m in dom f & f/.k in rng Line(G,i) & (for n st n in dom f & f/.n in rng Line(G,i) holds n<=k) & k<m & f/.m in rng Line(G,j) holds i<j; theorem :: GOBOARD1:46 f is_sequence_on G & i in dom f implies ex n st n in Seg width G & f/.i in rng Col(G,n); theorem :: GOBOARD1:47 f is_sequence_on G & i in dom f & i+1 in dom f & n in Seg width G & f/.i in rng Col(G,n) implies f/.(i+1) in rng Col(G,n) or for k st f/.(i+1) in rng Col(G,k) & k in Seg width G holds abs(n-k) = 1; theorem :: GOBOARD1:48 1<=len f & f/.len f in rng Col(G,width G) & f is_sequence_on G & i in Seg width G & i+1 in Seg width G & m in dom f & f/.m in rng Col(G,i) & (for k st k in dom f & f/.k in rng Col(G,i) holds k<=m) implies m+1 in dom f & f/.(m+1) in rng Col(G,i+1); theorem :: GOBOARD1:49 1<=len f & f/.1 in rng Col(G,1) & f/.len f in rng Col(G,width G) & f is_sequence_on G implies (for i st 1<=i & i<=width G holds ex k st k in dom f & f/.k in rng Col(G,i)) & (for i st 1<=i & i<=width G & 2<=len f holds L~f meets rng Col(G,i)) & for i,j,k,m st 1<=i & i<=width G & 1<=j & j<=width G & k in dom f & m in dom f & f/.k in rng Col(G,i) & (for n st n in dom f & f/.n in rng Col(G,i) holds n<=k) & k<m & f/.m in rng Col(G,j) holds i<j; theorem :: GOBOARD1:50 n in dom f & f/.n in rng Col(G,k) & k in Seg width G & f/.1 in rng Col(G,1) & f is_sequence_on G & (for i st i in dom f & f/.i in rng Col(G,k) holds n<=i) implies for i st i in dom f & i<=n holds for m st m in Seg width G & f/.i in rng Col(G,m) holds m<=k; theorem :: GOBOARD1:51 f is_sequence_on G & f/.1 in rng Col(G,1) & f/.len f in rng Col(G,width G) & width G > 1 & 1<=len f implies ex g st g/.1 in rng Col(DelCol(G,width G),1) & g/.len g in rng Col(DelCol(G,width G),width DelCol(G,width G)) & 1<=len g & g is_sequence_on DelCol(G,width G) & rng g c= rng f; theorem :: GOBOARD1:52 f is_sequence_on G & rng f /\ rng Col(G,1)<>{} & rng f /\ rng Col(G,width G)<>{} implies ex g st rng g c= rng f & g/.1 in rng Col(G,1) & g/.len g in rng Col(G,width G) & 1<=len g & g is_sequence_on G; theorem :: GOBOARD1:53 k in dom G & f is_sequence_on G & f/.len f in rng Line(G,len G) & n in dom f & f/.n in rng Line(G,k) implies (for i st k<=i & i<=len G ex j st j in dom f & n<=j & f/.j in rng Line(G,i)) & for i st k<i & i<=len G ex j st j in dom f & n<j & f/.j in rng Line(G,i);

Back to top