:: Introduction to Go-Board - Part I. Basic Notations
::  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, 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<i implies Col(
  DelCol(G,i),k) = Col(G,k) & k in Seg width DelCol(G,i) & k in Seg width G;

theorem :: GOBOARD1:14
  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:15
  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:16
  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: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<m & f/.m in rng Line(G,j)
  holds i<j;

theorem :: GOBOARD1:30
  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:31
  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 |.n-k.| = 1;

theorem :: GOBOARD1:32
  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:33
  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:34
  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:35
  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: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<i & i<=len G ex j st j in
  dom f & n<j & f/.j in rng Line(G,i);