The Mizar abstract of GOBOARD1

Journal of Formalized Mathematics
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);
The abstract of the Mizar article:

Introduction to Go-Board --- Part I
