The abstract of the Mizar article:

Decomposing a Go-Board into Cells

by

Yatsuka Nakamura, and

Andrzej Trybulec

Received May 26, 1995

MML identifier: GOBOARD5

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, MATRIX_1, FINSEQ_1, TREES_1, RELAT_1, MCART_1,
      GOBOARD1, SEQM_3, FUNCT_1, INCSP_1, ORDINAL2, BOOLE, TOPREAL1, GOBOARD2,
      FINSEQ_6, CARD_1, MATRIX_2, ABSVALUE, ARYTM_1, GOBOARD5, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, BINARITH, ABSVALUE, CARD_1, FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1,
      MATRIX_2, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
      FINSEQ_6;
 constructors DOMAIN_1, SEQM_3, REAL_1, BINARITH, ABSVALUE, MATRIX_2, TOPREAL1,
      GOBOARD2, FINSEQ_4, FINSEQ_6, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, GOBOARD1, GOBOARD2, MATRIX_1, EUCLID, FINSEQ_1,
      NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 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;

theorem :: GOBOARD5:1
 for M being tabular FinSequence, i,j st [i,j] in Indices M
   holds 1 <= i & i <= len M & 1 <= j & j <= width M;

definition let G be Matrix of TOP-REAL 2; let i;
 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:2
 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:3
 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:4
 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:5
 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:6
 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:7
 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:8
 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:9
 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:10
 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:11
 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;
 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 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;

definition
 cluster non constant special unfolded circular s.c.c.
           standard (non empty FinSequence of TOP-REAL 2);
end;

theorem :: GOBOARD5:12
 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:13
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 abs(m-i)+abs(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
 1 <= k & 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:14
 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:15
 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:16
 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:17
 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:18
 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:19
 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:20
 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:21
 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:22
 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:23
 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:24
 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:25
 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:26
 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:27
 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:28
 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: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,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:30
 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:31
 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:32
   1 <= k & k+1 <= len f implies left_cell(f,k) /\ right_cell(f,k) = LSeg(f,k);