:: Introduction to Go-Board - Part I. Basic Notations
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2016 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, COMPLEX1,
ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, NAT_1, RELAT_1, FINSEQ_3, FUNCT_1,
XBOOLE_0, TARSKI, ORDINAL2, PARTFUN1, MCART_1, TOPREAL1, RLTOPSP1,
MATRIX_1, TREES_1, INCSP_1, ZFMISC_1, ORDINAL4, GOBOARD1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, COMPLEX1, NAT_1,
VALUED_0, FINSEQ_1, FINSEQ_3, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1,
MATRIX_0, MATRIX_1;
constructors PARTFUN1, XXREAL_0, NAT_1, COMPLEX1, MATRIX_1, TOPREAL1, SEQM_3,
RELSET_1, REAL_1, MATRIX_0;
registrations RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
STRUCT_0, EUCLID, VALUED_0, INT_1;
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;
definition
let f;
func X_axis(f) -> FinSequence of REAL means
:: GOBOARD1:def 1
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 2
len it = len f & for n st n in dom it holds it.n = (f/.n)`2;
end;
theorem :: GOBOARD1:1
i in dom f & 2<=len f implies f/.i in L~f;
begin
:: Matrix preliminaries
definition
::$CD
let M be Matrix of TOP-REAL 2;
attr M is X_equal-in-line means
:: GOBOARD1:def 4
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 5
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 6
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 7
for n st n in Seg width M holds X_axis(Col(M,n)) is increasing;
end;
registration
cluster non empty-yielding X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column for Matrix of TOP-REAL 2;
end;
::$CT
theorem :: GOBOARD1:3
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:4
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:5
x=G*(m,k) & x=G*(i,j) & [m,k] in Indices G & [i,j] in Indices G
implies m=i & k=j;
::$CT 3
registration
let G;
let i be Nat;
cluster DelCol(G,i) -> X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column;
end;
::$CT 3
theorem :: GOBOARD1:12
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:13
i in Seg width G & width G = m+1 & m>0 & 1<=k & k*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:15
i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k**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:17
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:18
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:19
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:20
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:21
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
::$CD
let D,f,M;
pred f is_sequence_on M means
:: GOBOARD1:def 9
(for n st n in dom f ex i,j st [i,j] in Indices M & f/.n = M*(i,j)) &
:: rng F c= Values M
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 |.m-i.|+|.k-j.| = 1;
:: zmienic na egzystencjalny, to pierwszy warunek wypadnie.
end;
theorem :: GOBOARD1:22
(m in dom f implies 1 <= len(f|m)) &
(f is_sequence_on M implies f|m is_sequence_on M);
theorem :: GOBOARD1:23
(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:24
(for n st n in dom f1 & n+1 in dom f1
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 |.m-i.|+|.k-j.|=1) &
(for n st n in dom f2 & n+1 in dom f2
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 |.m-i.|+|.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 |.m-i.|+|.k-j.|=1)
implies
for n st n in dom(f1^f2) & n+1 in dom(f1^f2)
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 |.m-i.|+|.k-j.|=1;
reserve f for FinSequence of TOP-REAL 2;
theorem :: GOBOARD1:25
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:26
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:27
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 |.n-k.| = 1;
theorem :: GOBOARD1:28
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:29
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 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:36
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:37
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*