Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

The abstract of the Mizar article:

On the Go-Board of a Standard Special Circular Sequence

by
Andrzej Trybulec

Received October 15, 1995

MML identifier: GOBOARD7
[ Mizar article, MML identifier index ]


environ

 vocabulary FINSEQ_1, EUCLID, PRE_TOPC, GOBOARD1, ABSVALUE, ARYTM_1, TOPREAL1,
      MCART_1, ARYTM_3, MATRIX_1, TREES_1, RELAT_1, SPPOL_1, GOBOARD2, BOOLE,
      TOPS_1, GOBOARD5, TARSKI, SEQM_3, FUNCT_1, FINSET_1, CARD_1, FINSEQ_6,
      FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
      ABSVALUE, BINARITH, CARD_1, FUNCT_1, FINSEQ_1, FINSET_1, FINSEQ_4,
      MATRIX_1, PRE_TOPC, TOPS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
      SPPOL_1, FINSEQ_6, GOBOARD5, GROUP_1;
 constructors REAL_1, TOPS_1, SPPOL_1, GOBOARD2, GOBOARD5, SEQM_3, BINARITH,
      FINSEQ_4, GROUP_1, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, GOBOARD5, RELSET_1, GOBOARD2, INT_1, EUCLID, FINSEQ_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve f for non empty FinSequence of TOP-REAL 2,
        i,j,k,k1,k2,n,i1,i2,j1,j2 for Nat,
        r,s,r1,r2 for Real,
        p,q,p1,q1 for Point of TOP-REAL 2,
        G for Go-board,
        x for set;

theorem :: GOBOARD7:1
 abs(r1-r2) > s implies r1+s < r2 or r2+s < r1;

theorem :: GOBOARD7:2
abs(r - s) = 0 iff r = s;

theorem :: GOBOARD7:3
 for p,p1,q being Point of TOP-REAL n st p + p1 = q + p1
  holds p = q;

theorem :: GOBOARD7:4
  for p,p1,q being Point of TOP-REAL n st p1 + p = p1 + q
  holds p = q;

theorem :: GOBOARD7:5
 p1 in LSeg(p,q) & p`1 = q`1 implies p1`1 = q`1;

theorem :: GOBOARD7:6
 p1 in LSeg(p,q) & p`2 = q`2 implies p1`2 = q`2;

theorem :: GOBOARD7:7
 1/2*(p+q) in LSeg(p,q);

theorem :: GOBOARD7:8
 p`1 = q`1 & q`1 = p1`1 & p`2 <= q`2 & q`2 <= p1`2 implies q in LSeg(p,p1);

theorem :: GOBOARD7:9
 p`1 <= q`1 & q`1 <= p1`1 & p`2 = q`2 & q`2 = p1`2 implies q in LSeg(p,p1);

theorem :: GOBOARD7:10
 for D being non empty set
 for i,j for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M
  holds [i,j] in Indices M;

theorem :: GOBOARD7:11
   1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  1/2*(G*(i,j)+G*(i+1,j+1)) = 1/2*(G*(i,j+1)+G*(i+1,j));

theorem :: GOBOARD7:12
 LSeg(f,k) is horizontal implies
  ex j st 1 <= j & j <= width GoB f &
   for p st p in LSeg(f,k) holds p`2 = (GoB f)*(1,j)`2;

theorem :: GOBOARD7:13
 LSeg(f,k) is vertical implies
  ex i st 1 <= i & i <= len GoB f &
   for p st p in LSeg(f,k) holds p`1 = (GoB f)*(i,1)`1;

theorem :: GOBOARD7:14
   f is special & i <= len GoB f & j <= width GoB f implies
  Int cell(GoB f,i,j) misses L~f;

begin :: Segments on a Go Board

theorem :: GOBOARD7:15
 1 <= i & i <= len G & 1 <= j & j+2 <= width G implies
  LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2)) = { G*(i,j+1) };

theorem :: GOBOARD7:16
 1 <= i & i+2 <= len G & 1 <= j & j <= width G implies
  LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j)) = { G*(i+1,j) };

theorem :: GOBOARD7:17
 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1)) = { G*(i,j+1) };

theorem :: GOBOARD7:18
 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  LSeg(G*(i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*
(i+1,j+1) };

theorem :: GOBOARD7:19
 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G*(i,j+1)) = { G*(i,j) };

theorem :: GOBOARD7:20
 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*(i+1,j) };

theorem :: GOBOARD7:21
 for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
  1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
  LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1))
 holds i1 = i2 & abs(j1-j2) <= 1;

theorem :: GOBOARD7:22
 for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
  1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
  LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
 holds j1 = j2 & abs(i1-i2) <= 1;

theorem :: GOBOARD7:23
 for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
  1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
  LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
 holds (i1 = i2 or i1 = i2+1) & (j1 = j2 or j1+1 = j2);

theorem :: GOBOARD7:24
   for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
  1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
  LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1))
 holds
  j1 = j2 &
  LSeg(G*(i1,j1),G*(i1,j1+1)) = LSeg(G*(i2,j2),G*(i2,j2+1)) or
  j1 = j2+1 &
  LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G*
(i1,j1) }
  or j1+1 = j2 &
  LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G*
(i2,j2) };

theorem :: GOBOARD7:25
   for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
  1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
  LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
 holds
  i1 = i2 &
  LSeg(G*(i1,j1),G*(i1+1,j1)) = LSeg(G*(i2,j2),G*(i2+1,j2)) or
  i1 = i2+1 &
  LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1) }
  or i1+1 = i2 &
  LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i2,j2) };

theorem :: GOBOARD7:26
   for i1,j1,i2,j2 being Nat st
  1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
  1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
  LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
 holds
  j1 = j2 &
  LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1) }
  or j1+1 = j2 &
  LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1+1) };

theorem :: GOBOARD7:27
 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
  1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*(i2,j2),G*(i2,j2+1)) implies
    i1 = i2 & j1 = j2;


theorem :: GOBOARD7:28
 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
  1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*(i2,j2),G*(i2+1,j2)) implies
    i1 = i2 & j1 = j2;

theorem :: GOBOARD7:29
 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G implies
 not ex i2,j2 st
  1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
   1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*(i2,j2),G*(i2,j2+1));

theorem :: GOBOARD7:30
 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G implies
 not ex i2,j2 st
  1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
   1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*(i2,j2),G*(i2+1,j2));

begin :: Standard special circular sequences

reserve f for non constant standard special_circular_sequence;

theorem :: GOBOARD7:31
 for f being standard (non empty FinSequence of TOP-REAL 2)
  st i in dom f & i+1 in dom f holds f/.i <> f/.(i+1);

theorem :: GOBOARD7:32
 ex i st i in dom f & (f/.i)`1 <> (f/.1)`1;

theorem :: GOBOARD7:33
 ex i st i in dom f & (f/.i)`2 <> (f/.1)`2;

theorem :: GOBOARD7:34
   len GoB f > 1;

theorem :: GOBOARD7:35
   width GoB f > 1;

theorem :: GOBOARD7:36
 len f > 4;

theorem :: GOBOARD7:37
 for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f > 4
  for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j;

theorem :: GOBOARD7:38
  for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j;

theorem :: GOBOARD7:39
  for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j;

theorem :: GOBOARD7:40
  for i being Nat st 1 < i & i <= len f & f/.i = f/.1 holds i = len f;

theorem :: GOBOARD7:41
 1 <= i & i <= len GoB f & 1 <= j & j+1 <= width GoB f &
  1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in L~f implies
 ex k st 1 <= k & k+1 <= len f &
  LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k);

theorem :: GOBOARD7:42
   1 <= i & i+1 <= len GoB f & 1 <= j & j <= width GoB f &
    1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in L~f implies
   ex k st 1 <= k & k+1 <= len f &
    LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k);

theorem :: GOBOARD7:43
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) &
  f/.(k+2) = (GoB f)*(i+1,j);

theorem :: GOBOARD7:44
   1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f
&
 LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j+2) & f/.(k+1) = (GoB f)*(i,j+1) &
  f/.(k+2) = (GoB f)*(i,j);

theorem :: GOBOARD7:45
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i,j+1) &
  f/.(k+2) = (GoB f)*(i,j);

theorem :: GOBOARD7:46
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) &
  f/.(k+2) = (GoB f)*(i,j+1);

theorem :: GOBOARD7:47
   1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f
&
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i+2,j) & f/.(k+1) = (GoB f)*(i+1,j) &
  f/.(k+2) = (GoB f)*(i,j);

theorem :: GOBOARD7:48
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i+1,j) &
  f/.(k+2) = (GoB f)*(i,j);

theorem :: GOBOARD7:49
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) &
  f/.(k+2) = (GoB f)*(i,j+1);

theorem :: GOBOARD7:50
   1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f
&
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i,j+1) &
  f/.(k+2) = (GoB f)*(i,j+2);

theorem :: GOBOARD7:51
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i,j+1) &
  f/.(k+2) = (GoB f)*(i+1,j+1);

theorem :: GOBOARD7:52
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) &
  f/.(k+2) = (GoB f)*(i+1,j);

theorem :: GOBOARD7:53
   1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f
&
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i+1,j) &
  f/.(k+2) = (GoB f)*(i+2,j);

theorem :: GOBOARD7:54
   1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
 k & k+1 < len f &
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
  f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i+1,j) &
  f/.(k+2) = (GoB f)*(i+1,j+1);

theorem :: GOBOARD7:55
 1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f &
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f implies
  f/.1 = (GoB f)*(i,j+1) &
  (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i,j+2) or
   f/.2 = (GoB f)*(i,j+2) & f/.(len f-'1) = (GoB f)*(i,j))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) &
   (f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i,j+2) or
    f/.k = (GoB f)*(i,j+2) & f/.(k+2) = (GoB f)*(i,j));

theorem :: GOBOARD7:56
 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
 LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f implies
  f/.1 = (GoB f)*(i,j+1) &
  (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or
   f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) &
   (f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or
    f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j));

theorem :: GOBOARD7:57
 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
 LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f &
 LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,j)) c= L~f implies
  f/.1 = (GoB f)*(i+1,j+1) &
  (f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+1,j) or
   f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,j+1))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) &
   (f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or
    f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1));

theorem :: GOBOARD7:58
 1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f &
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f implies
  f/.1 = (GoB f)*(i+1,j) &
  (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+2,j) or
   f/.2 = (GoB f)*(i+2,j) & f/.(len f-'1) = (GoB f)*(i,j))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) &
   (f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+2,j) or
    f/.k = (GoB f)*(i+2,j) & f/.(k+2) = (GoB f)*(i,j));

theorem :: GOBOARD7:59
 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
 LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f implies
  f/.1 = (GoB f)*(i+1,j) &
  (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or
   f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) &
   (f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or
    f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j));

theorem :: GOBOARD7:60
 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
 LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f &
 LSeg((GoB f)*(i+1,j+1),(GoB f)*(i,j+1)) c= L~f implies
  f/.1 = (GoB f)*(i+1,j+1) &
  (f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,j+1) or
   f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+1,j))
  or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j+1) &
   (f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or
    f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j));

theorem :: GOBOARD7:61
   1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies
  not ( LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
        LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f &
        LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f);

theorem :: GOBOARD7:62
   1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies
  not ( LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f &
        LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,j+2)) c= L~f &
        LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f);

theorem :: GOBOARD7:63
   1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies
  not ( LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
        LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f &
        LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f);

theorem :: GOBOARD7:64
   1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies
  not ( LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f &
        LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+2,j+1)) c= L~f &
        LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f);


Back to top