:: Decomposing a Go Board into Cells
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received May 26, 1995
:: Copyright (c) 1995-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, SUBSET_1, REAL_1, MATRIX_1, NAT_1,
      RELAT_1, MCART_1, XXREAL_0, ARYTM_3, FINSEQ_1, TARSKI, STRUCT_0, TREES_1,
      GOBOARD1, FUNCT_1, PARTFUN1, INCSP_1, ORDINAL2, CARD_1, XBOOLE_0,
      RLTOPSP1, GOBOARD2, TOPREAL1, FINSEQ_6, ORDINAL4, ZFMISC_1, COMPLEX1,
      ARYTM_1, GOBOARD5, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ZFMISC_1, CARD_1, ORDINAL1,
      NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1,
      PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, MATRIX_1, SEQM_3, SEQ_4,
      STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
      FINSEQ_6, XXREAL_0;
 constructors PARTFUN1, ENUMSET1, XXREAL_0, NAT_1, COMPLEX1, FINSEQ_4, NAT_D,
      FINSEQ_6, MATRIX_1, TOPREAL1, GOBOARD2, GOBOARD1, SEQM_3, RELSET_1,
      REAL_1, SEQ_4, RVSUM_1;
 registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID,
      GOBOARD2, VALUED_0, SEQ_4, ORDINAL1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve p,q for Point of TOP-REAL 2,
  i,i1,i2,j,j1,j2,k for Nat,
  r,s for Real,
  G for Matrix of TOP-REAL 2;

definition
  let G be Matrix of TOP-REAL 2;
  let i be Nat;
  func v_strip(G,i) -> Subset of TOP-REAL 2 equals
:: GOBOARD5:def 1

  { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 } if 1 <= i & i < len G,
  { |[r,s]| : G*(i,1)`1 <= r } if i >= len G
  otherwise { |[r,s]| : r <= G*(i+1,1)`1 };
  func h_strip(G,i) -> Subset of TOP-REAL 2 equals
:: GOBOARD5:def 2

  { |[r,s]| : G*(1,i)`2 <= s & s <= G*(1,i+1)`2 } if 1 <= i & i < width G,
  { |[r,s]| : G*(1,i)`2 <= s } if i >= width G
  otherwise { |[r,s]| : s <= G*(1,i+1)`2 };
end;

theorem :: GOBOARD5:1
  G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G
  implies G*(i,j)`2 = G*(1,j)`2;

theorem :: GOBOARD5:2
  G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G
  implies G*(i,j)`1 = G*(i,1)`1;

theorem :: GOBOARD5:3
  G is X_increasing-in-column &
  1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G
  implies G*(i1,j)`1 < G*(i2,j)`1;

theorem :: GOBOARD5:4
  G is Y_increasing-in-line &
  1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G
  implies G*(i,j1)`2 < G*(i,j2)`2;

theorem :: GOBOARD5:5
  G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G
  implies h_strip(G,j) = { |[r,s]| : G*(i,j)`2 <= s & s <= G*(i,j+1)`2 };

theorem :: GOBOARD5:6
  G is non empty-yielding Y_equal-in-column & 1 <= i & i <= len G
  implies h_strip(G,width G) = { |[r,s]| : G*(i,width G)`2 <= s };

theorem :: GOBOARD5:7
  G is non empty-yielding Y_equal-in-column & 1 <= i & i <= len G
  implies h_strip(G,0) = { |[r,s]| : s <= G*(i,1)`2 };

theorem :: GOBOARD5:8
  G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G
  implies v_strip(G,i) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 };

theorem :: GOBOARD5:9
  G is non empty-yielding X_equal-in-line & 1 <= j & j <= width G
  implies v_strip(G,len G) = { |[r,s]| : G*(len G,j)`1 <= r };

theorem :: GOBOARD5:10
  G is non empty-yielding X_equal-in-line & 1 <= j & j <= width G
  implies v_strip(G,0) = { |[r,s]| : r <= G*(1,j)`1 };

definition
  let G be Matrix of TOP-REAL 2;
  let i,j be Nat;
  func cell(G,i,j) -> Subset of TOP-REAL 2 equals
:: GOBOARD5:def 3
  v_strip(G,i) /\ h_strip(G,j);
end;

definition
  let IT be FinSequence of TOP-REAL 2;
  attr IT is s.c.c. means
:: GOBOARD5:def 4
  for i,j being Nat st i+1 < j & (i > 1 & j < len IT or j+1 < len IT)
  holds LSeg(IT,i) misses LSeg(IT,j);
end;

definition
  let IT be non empty FinSequence of TOP-REAL 2;
  attr IT is standard means
:: GOBOARD5:def 5

  IT is_sequence_on GoB IT;
end;

registration
  cluster non constant special unfolded circular s.c.c.
    standard for non empty FinSequence of TOP-REAL 2;
end;

theorem :: GOBOARD5:11
  for f being non empty FinSequence of TOP-REAL 2
  for n being Nat st n in dom f
  ex i,j st [i,j] in Indices GoB f & f/.n = (GoB f)*(i,j);

theorem :: GOBOARD5:12
  for f being standard non empty FinSequence of TOP-REAL 2,
  n being Nat st n in dom f & n+1 in dom f
  for m,k,i,j being Nat
  st [m,k] in Indices GoB f & [i,j] in Indices GoB f &
  f/.n = (GoB f)*(m,k) & f/.(n+1) = (GoB f)*(i,j) holds |.m-i.|+|.k-j.| = 1;

definition
  mode special_circular_sequence is
    special unfolded circular s.c.c. non empty FinSequence of TOP-REAL 2;
end;

reserve f for standard special_circular_sequence;

definition
  let f,k;
  assume that
 1 <= k and
 k+1 <= len f;
  func right_cell(f,k) -> Subset of TOP-REAL 2 means
:: GOBOARD5:def 6

  for i1,j1,i2,j2 being Nat st
  [i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
  f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
  i1 = i2 & j1+1 = j2 & it = cell(GoB f,i1,j1) or
  i1+1 = i2 & j1 = j2 & it = cell(GoB f,i1,j1-'1) or
  i1 = i2+1 & j1 = j2 & it = cell(GoB f,i2,j2) or
  i1 = i2 & j1 = j2+1 & it = cell(GoB f,i1-'1,j2);
  func left_cell(f,k) -> Subset of TOP-REAL 2 means
:: GOBOARD5:def 7

  for i1,j1,i2,j2 being Nat  st
  [i1,j1] in Indices GoB f & [i2,j2] in Indices GoB f &
  f/.k = (GoB f)*(i1,j1) & f/.(k+1) = (GoB f)*(i2,j2) holds
  i1 = i2 & j1+1 = j2 & it = cell(GoB f,i1-'1,j1) or
  i1+1 = i2 & j1 = j2 & it = cell(GoB f,i1,j1) or
  i1 = i2+1 & j1 = j2 & it = cell(GoB f,i2,j2-'1) or
  i1 = i2 & j1 = j2+1 & it = cell(GoB f,i1,j2);
end;

theorem :: GOBOARD5:13
  G is non empty-yielding X_equal-in-line X_increasing-in-column &
  i < len G & 1 <= j & j < width G
  implies LSeg(G*(i+1,j),G*(i+1,j+1)) c= v_strip(G,i);

theorem :: GOBOARD5:14
  G is non empty-yielding X_equal-in-line X_increasing-in-column &
  1 <= i & i <= len G & 1 <= j & j < width G
  implies LSeg(G*(i,j),G*(i,j+1)) c= v_strip(G,i);

theorem :: GOBOARD5:15
  G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
  j < width G & 1 <= i & i < len G
  implies LSeg(G*(i,j+1),G*(i+1,j+1)) c= h_strip(G,j);

theorem :: GOBOARD5:16
  G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
  1 <= j & j <= width G & 1 <= i & i < len G
  implies LSeg(G*(i,j),G*(i+1,j)) c= h_strip(G,j);

theorem :: GOBOARD5:17
  G is Y_equal-in-column Y_increasing-in-line &
  1 <= i & i <= len G & 1 <= j & j+1 <= width G
  implies LSeg(G*(i,j),G*(i,j+1)) c= h_strip(G,j);

theorem :: GOBOARD5:18
  for G being Go-board holds i < len G & 1 <= j & j < width G
  implies LSeg(G*(i+1,j),G*(i+1,j+1)) c= cell(G,i,j);

theorem :: GOBOARD5:19
  for G being Go-board holds 1 <= i & i <= len G & 1 <= j & j < width G
  implies LSeg(G*(i,j),G*(i,j+1)) c= cell(G,i,j);

theorem :: GOBOARD5:20
  G is X_equal-in-line X_increasing-in-column &
  1 <= j & j <= width G & 1 <= i & i+1 <= len G
  implies LSeg(G*(i,j),G*(i+1,j)) c= v_strip(G,i);

theorem :: GOBOARD5:21
  for G being Go-board holds j < width G & 1 <= i & i < len G
  implies LSeg(G*(i,j+1),G*(i+1,j+1)) c= cell(G,i,j);

theorem :: GOBOARD5:22
  for G being Go-board holds 1 <= i & i < len G & 1 <= j & j <= width G
  implies LSeg(G*(i,j),G*(i+1,j)) c= cell(G,i,j);

theorem :: GOBOARD5:23
  G is non empty-yielding X_equal-in-line X_increasing-in-column &
  i+1 <= len G implies
  v_strip(G,i) /\ v_strip(G,i+1) = { q : q`1 = G*(i+1,1)`1 };

theorem :: GOBOARD5:24
  G is non empty-yielding Y_equal-in-column Y_increasing-in-line &
  j+1 <= width G implies
  h_strip(G,j) /\ h_strip(G,j+1) = { q : q`2 = G*(1,j+1)`2 };

theorem :: GOBOARD5:25
  for G being Go-board holds i < len G & 1 <= j & j < width G
  implies cell(G,i,j) /\ cell(G,i+1,j) = LSeg(G*(i+1,j),G*(i+1,j+1));

theorem :: GOBOARD5:26
  for G being Go-board holds j < width G & 1 <= i & i < len G
  implies cell(G,i,j) /\ cell(G,i,j+1) = LSeg(G*(i,j+1),G*(i+1,j+1));

theorem :: GOBOARD5:27
  1 <= k & k+1 <= len f & [i+1,j] in Indices GoB f & [i+1,j+1] in
  Indices GoB f &
  f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) implies
  left_cell(f,k) = cell(GoB f,i,j) & right_cell(f,k) = cell(GoB f,i+1,j);

theorem :: GOBOARD5:28
  1 <= k & k+1 <= len f & [i,j+1] in Indices GoB f & [i+1,j+1] in
  Indices GoB f &
  f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) implies
  left_cell(f,k) = cell(GoB f,i,j+1) & right_cell(f,k) = cell(GoB f,i,j);

theorem :: GOBOARD5:29
  1 <= k & k+1 <= len f & [i,j+1] in Indices GoB f & [i+1,j+1] in
  Indices GoB f &
  f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i,j+1) implies
  left_cell(f,k) = cell(GoB f,i,j) & right_cell(f,k) = cell(GoB f,i,j+1);

theorem :: GOBOARD5:30
  1 <= k & k+1 <= len f & [i+1,j+1] in Indices GoB f & [i+1,j] in
  Indices GoB f &
  f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i+1,j) implies
  left_cell(f,k) = cell(GoB f,i+1,j) & right_cell(f,k) = cell(GoB f,i,j);

theorem :: GOBOARD5:31
  1 <= k & k+1 <= len f implies left_cell(f,k) /\ right_cell(f,k) = LSeg(f, k )
;