The abstract of the Mizar article:

On the Geometry of a Go-Board

by

Andrzej Trybulec

Received July 9, 1995

MML identifier: GOBOARD6

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, GOBOARD1, MCART_1, ARYTM_1, METRIC_1, PCOMPS_1,
      TOPS_1, SQUARE_1, FUNCT_1, FINSEQ_1, TREES_1, GOBOARD5, ARYTM_3,
      ABSVALUE, BOOLE, TOPREAL1, ARYTM;
 notation TARSKI, XBOOLE_0, ORDINAL1, XREAL_0, REAL_1, NAT_1, ABSVALUE,
      SQUARE_1, BINARITH, BINOP_1, FINSEQ_1, MATRIX_1, STRUCT_0, METRIC_1,
      PRE_TOPC, TOPS_1, PCOMPS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5;
 constructors REAL_1, ABSVALUE, SQUARE_1, BINARITH, TOPS_1, PCOMPS_1, GOBOARD1,
      GOBOARD5, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, EUCLID, XREAL_0, PCOMPS_1, METRIC_1, ARYTM_3,
      MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve i,j,n for Nat,
        r,s,r1,s1,r2,s2,r',s' for Real,
        p,q for Point of TOP-REAL 2,
        G for Go-board,
        x,y for set,
        v for Point of Euclid 2;

canceled 3;

theorem :: GOBOARD6:4
 for M being non empty Reflexive MetrStruct, u being Point of M,
     r being real number holds
  r > 0 implies u in Ball(u,r);

canceled;

theorem :: GOBOARD6:6
 for B being Subset of TOP-REAL n, u being Point of Euclid n
    st B = Ball(u,r) holds B is open;

theorem :: GOBOARD6:7
 for M being non empty MetrSpace, u being Point of M,
     P being Subset of TopSpaceMetr(M)
  holds u in Int P iff ex r being real number st r > 0 & Ball(u,r) c= P;

theorem :: GOBOARD6:8
 for u being Point of Euclid n, P being Subset of TOP-REAL n
  holds u in Int P iff ex r being real number st r > 0 & Ball(u,r) c= P;

theorem :: GOBOARD6:9  :: TOPREAL3:12
 for u,v being Point of Euclid 2 st u = |[r1,s1]| & v = |[r2,s2]| holds
  dist(u,v) =sqrt ((r1 - r2)^2 + (s1 - s2)^2);

theorem :: GOBOARD6:10
 for u being Point of Euclid 2 st u = |[r,s]| holds
 0 <= r2 & r2 < r1 implies |[r+r2,s]| in Ball(u,r1);

theorem :: GOBOARD6:11
 for u being Point of Euclid 2 st u = |[r,s]| holds
 0 <= s2 & s2 < s1 implies |[r,s+s2]| in Ball(u,s1);

theorem :: GOBOARD6:12
 for u being Point of Euclid 2 st u = |[r,s]| holds
 0 <= r2 & r2 < r1 implies |[r-r2,s]| in Ball(u,r1);

theorem :: GOBOARD6:13
 for u being Point of Euclid 2 st u = |[r,s]| holds
 0 <= s2 & s2 < s1 implies |[r,s-s2]| in Ball(u,s1);

theorem :: GOBOARD6:14
 1 <= i & i < len G & 1 <= j & j < width G
   implies G*(i,j)+G*(i+1,j+1) = G*(i,j+1)+G*(i+1,j);

theorem :: GOBOARD6:15
 Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 };

theorem :: GOBOARD6:16
 Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r };

theorem :: GOBOARD6:17
 1 <= i & i < len G
  implies Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 };

theorem :: GOBOARD6:18
 Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 };

theorem :: GOBOARD6:19
 Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s };

theorem :: GOBOARD6:20
 1 <= j & j < width G
  implies Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:21
 Int cell(G,0,0) = { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 };

theorem :: GOBOARD6:22
 Int cell(G,0,width G) = { |[r,s]| : r < G*(1,1)`1 & G*(1,width G)`2 < s };

theorem :: GOBOARD6:23
 1 <= j & j < width G
  implies Int cell(G,0,j) =
    { |[r,s]| : r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:24
 Int cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1)`2 };

theorem :: GOBOARD6:25
 Int cell(G,len G,width G) =
    { |[r,s]| : G*(len G,1)`1 < r & G*(1,width G)`2 < s };

theorem :: GOBOARD6:26
 1 <= j & j < width G
  implies Int cell(G,len G,j) =
    { |[r,s]| : G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:27
 1 <= i & i < len G
  implies Int cell(G,i,0) =
    { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 };

theorem :: GOBOARD6:28
 1 <= i & i < len G
  implies Int cell(G,i,width G) =
    { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s };

theorem :: GOBOARD6:29
 1 <= i & i < len G & 1 <= j & j < width G
  implies Int cell(G,i,j) =
    { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 &
                G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:30
  1 <= j & j <= width G & p in Int h_strip(G,j) implies p`2 > G*(1,j)`2;

theorem :: GOBOARD6:31
  j < width G & p in Int h_strip(G,j) implies p`2 < G*(1,j+1)`2;

theorem :: GOBOARD6:32
  1 <= i & i <= len G & p in Int v_strip(G,i) implies p`1 > G*(i,1)`1;

theorem :: GOBOARD6:33
  i < len G & p in Int v_strip(G,i) implies p`1 < G*(i+1,1)`1;

theorem :: GOBOARD6:34
 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  1/2*(G*(i,j)+G*(i+1,j+1)) in Int cell(G,i,j);

theorem :: GOBOARD6:35
 1 <= i & i+1 <= len G implies
  1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]| in Int cell(G,i,width G);

theorem :: GOBOARD6:36
 1 <= i & i+1 <= len G implies
  1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| in Int cell(G,i,0);

theorem :: GOBOARD6:37
 1 <= j & j+1 <= width G implies
  1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]| in Int cell(G,len G,j);

theorem :: GOBOARD6:38
 1 <= j & j+1 <= width G implies
  1/2*(G*(1,j)+G*(1,j+1))-|[1,0]| in Int cell(G,0,j);

theorem :: GOBOARD6:39
  G*(1,1)-|[1,1]| in Int cell(G,0,0);

theorem :: GOBOARD6:40
  G*(len G,width G)+|[1,1]| in Int cell(G,len G,width G);

theorem :: GOBOARD6:41
  G*(1,width G)+|[-1,1]| in Int cell(G,0,width G);

theorem :: GOBOARD6:42
  G*(len G,1)+|[1,-1]| in Int cell(G,len G,0);

theorem :: GOBOARD6:43
 1 <= i & i < len G & 1 <= j & j < width G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i,j+1)))
    c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i,j+1)) };

theorem :: GOBOARD6:44
 1 <= i & i < len G & 1 <= j & j < width G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+1))) c=
      Int cell(G,i,j) \/ { 1/2*(G*(i,j+1)+G*(i+1,j+1)) };

theorem :: GOBOARD6:45
 1 <= i & i < len G & 1 <= j & j < width G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+1,j+1))) c=
      Int cell(G,i,j) \/ { 1/2*(G*(i+1,j)+G*(i+1,j+1)) };

theorem :: GOBOARD6:46
 1 <= i & i < len G & 1 <= j & j < width G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i+1,j))) c=
      Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i+1,j)) };

theorem :: GOBOARD6:47
 1 <= j & j < width G implies
 LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,1/2*(G*(1,j)+G*(1,j+1))) c=
      Int cell(G,0,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) };

theorem :: GOBOARD6:48
 1 <= j & j < width G implies
 LSeg(1/2*(G*(len G,j)+G*(len G,j+1))
       + |[1,0]|,1/2*(G*(len G,j)+G*(len G,j+1)))
   c= Int cell(G,len G,j) \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) };

theorem :: GOBOARD6:49
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,1/2*(G*(i,1)+G*(i+1,1))) c=
      Int cell(G,i,0) \/ { 1/2*(G*(i,1)+G*(i+1,1)) };

theorem :: GOBOARD6:50
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+ |[0,1]|,
      1/2*(G*(i,width G)+G*(i+1,width G)))
   c= Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) };

theorem :: GOBOARD6:51
 1 <= j & j < width G implies
 LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,G*(1,j) - |[1,0]|) c=
      Int cell(G,0,j) \/ { G*(1,j) - |[1,0]| };

theorem :: GOBOARD6:52
 1 <= j & j < width G implies
 LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,G*(1,j+1) - |[1,0]|) c=
      Int cell(G,0,j) \/ { G*(1,j+1) - |[1,0]| };

theorem :: GOBOARD6:53
 1 <= j & j < width G implies
 LSeg(1/2*(G*(len G,j)+G*(len G,j+1)) + |[1,0]|,G*(len G,j) + |[1,0]|) c=
      Int cell(G,len G,j) \/ { G*(len G,j) + |[1,0]| };

theorem :: GOBOARD6:54
 1 <= j & j < width G implies
 LSeg(1/2*(G*(len G,j)+G*(len G,j+1)) + |[1,0]|,G*(len G,j+1) + |[1,0]|) c=
      Int cell(G,len G,j) \/ { G*(len G,j+1) + |[1,0]| };

theorem :: GOBOARD6:55
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,G*(i,1) - |[0,1]|) c=
      Int cell(G,i,0) \/ { G*(i,1) - |[0,1]| };

theorem :: GOBOARD6:56
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,G*(i+1,1) - |[0,1]|) c=
      Int cell(G,i,0) \/ { G*(i+1,1) - |[0,1]| };

theorem :: GOBOARD6:57
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G*
(i,width G) + |[0,1]|) c=
      Int cell(G,i,width G) \/ { G*(i,width G) + |[0,1]| };

theorem :: GOBOARD6:58
 1 <= i & i < len G implies
 LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G*
(i+1,width G) + |[0,1]|)
    c= Int cell(G,i,width G) \/ { G*(i+1,width G) + |[0,1]| };

theorem :: GOBOARD6:59
 LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[1,0]|) c=
      Int cell(G,0,0) \/ { G*(1,1) - |[1,0]| };

theorem :: GOBOARD6:60
 LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) + |[1,0]|) c=
      Int cell(G,len G,0) \/ { G*(len G,1) + |[1,0]| };

theorem :: GOBOARD6:61
 LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) - |[1,0]|) c=
      Int cell(G,0,width G) \/ { G*(1,width G) - |[1,0]| };

theorem :: GOBOARD6:62
 LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[1,0]|) c=
      Int cell(G,len G,width G) \/ { G*(len G,width G) + |[1,0]| };

theorem :: GOBOARD6:63
 LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[0,1]|) c=
      Int cell(G,0,0) \/ { G*(1,1) - |[0,1]| };

theorem :: GOBOARD6:64
 LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) - |[0,1]|) c=
      Int cell(G,len G,0) \/ { G*(len G,1) - |[0,1]| };

theorem :: GOBOARD6:65
 LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) + |[0,1]|) c=
      Int cell(G,0,width G) \/ { G*(1,width G) + |[0,1]| };

theorem :: GOBOARD6:66
 LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[0,1]|) c=
      Int cell(G,len G,width G) \/ { G*(len G,width G) + |[0,1]| };

theorem :: GOBOARD6:67
   1 <= i & i < len G & 1 <= j & j+1 < width G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+2))) c=
  Int cell(G,i,j) \/ Int cell(G,i,j+1) \/ { 1/2*(G*(i,j+1)+G*(i+1,j+1)) };

theorem :: GOBOARD6:68
   1 <= j & j < width G & 1 <= i & i+1 < len G implies
 LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+2,j+1))) c=
  Int cell(G,i,j) \/ Int cell(G,i+1,j) \/ { 1/2*(G*(i+1,j)+G*(i+1,j+1)) };

theorem :: GOBOARD6:69
   1 <= i & i < len G & 1 < width G implies
 LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,1/2*(G*(i,1)+G*(i+1,2))) c=
  Int cell(G,i,0) \/ Int cell(G,i,1) \/ { 1/2*(G*(i,1)+G*(i+1,1)) };

theorem :: GOBOARD6:70
   1 <= i & i < len G & 1 < width G implies
 LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|,
      1/2*(G*(i,width G)+G*(i+1,width G -' 1))) c=
  Int cell(G,i,width G -'1) \/ Int cell(G,i,width G)
        \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) };

theorem :: GOBOARD6:71
   1 <= j & j < width G & 1 < len G implies
 LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,1/2*(G*(1,j)+G*(2,j+1))) c=
  Int cell(G,0,j) \/ Int cell(G,1,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) };

theorem :: GOBOARD6:72
   1 <= j & j < width G & 1 < len G implies
 LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|,
      1/2*(G*(len G,j)+G*(len G -' 1,j+1))) c=
  Int cell(G,len G -' 1,j) \/ Int cell(G,len G,j)
        \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) };

theorem :: GOBOARD6:73
   1 < len G & 1 <= j & j+1 < width G implies
 LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,1/2*(G*(1,j+1)+G*(1,j+2))-|[1,0]|) c=
  Int cell(G,0,j) \/ Int cell(G,0,j+1) \/ { G*(1,j+1)-|[1,0]| };

theorem :: GOBOARD6:74
   1 < len G & 1 <= j & j+1 < width G implies
 LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|,
      1/2*(G*(len G,j+1)+G*(len G,j+2))+|[1,0]|) c=
  Int cell(G,len G,j) \/ Int cell(G,len G,j+1) \/ { G*(len G,j+1)+|[1,0]| };

theorem :: GOBOARD6:75
   1 < width G & 1 <= i & i+1 < len G implies
 LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,1/2*(G*(i+1,1)+G*(i+2,1))-|[0,1]|) c=
  Int cell(G,i,0) \/ Int cell(G,i+1,0) \/ { G*(i+1,1)-|[0,1]| };

theorem :: GOBOARD6:76
   1 < width G & 1 <= i & i+1 < len G implies
 LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|,
      1/2*(G*(i+1,width G)+G*(i+2,width G))+|[0,1]|) c=
  Int cell(G,i,width G) \/ Int cell(G,i+1,width G) \/
 { G*(i+1,width G)+|[0,1]| };

theorem :: GOBOARD6:77
   1 < len G & 1 < width G implies
 LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(1,2))-|[1,0]|) c=
  Int cell(G,0,0) \/ Int cell(G,0,1) \/ { G*(1,1)-|[1,0]| };

theorem :: GOBOARD6:78
   1 < len G & 1 < width G implies
 LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len G,1)+G*(len G,2))+|[1,0]|) c=
  Int cell(G,len G,0) \/ Int cell(G,len G,1) \/ { G*(len G,1)+|[1,0]| };

theorem :: GOBOARD6:79
   1 < len G & 1 < width G implies
 LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1,width G)+G*
(1,width G -' 1))-|[1,0]|) c=
  Int cell(G,0,width G) \/ Int cell(G,0,width G -' 1)
                        \/ { G*(1,width G)-|[1,0]| };

theorem :: GOBOARD6:80
   1 < len G & 1 < width G implies
 LSeg(G*(len G,width G)+|[1,1]|,
      1/2*(G*(len G,width G)+G*(len G,width G -' 1))+|[1,0]|) c=
  Int cell(G,len G,width G) \/ Int cell(G,len G,width G -' 1)
              \/ { G*(len G,width G)+|[1,0]| };

theorem :: GOBOARD6:81
   1 < width G & 1 < len G implies
 LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(2,1))-|[0,1]|) c=
  Int cell(G,0,0) \/ Int cell(G,1,0) \/ { G*(1,1)-|[0,1]| };

theorem :: GOBOARD6:82
   1 < width G & 1 < len G implies
 LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1,width G)+G*(2,width G))+|[0,1]|) c=
  Int cell(G,0,width G) \/ Int cell(G,1,width G) \/ { G*(1,width G)+|[0,1]| };

theorem :: GOBOARD6:83
   1 < width G & 1 < len G implies
 LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len G,1)+G*(len G -' 1,1))-|[0,1]|) c=
  Int cell(G,len G,0) \/ Int cell(G,len G -' 1,0)
                        \/ { G*(len G,1)-|[0,1]| };

theorem :: GOBOARD6:84
   1 < width G & 1 < len G implies
 LSeg(G*(len G,width G)+|[1,1]|,
      1/2*(G*(len G,width G)+G*(len G -' 1,width G))+|[0,1]|) c=
  Int cell(G,len G,width G) \/ Int cell(G,len G -' 1,width G)
              \/ { G*(len G,width G)+|[0,1]| };

theorem :: GOBOARD6:85
   1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
  LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),p) meets Int cell(G,i,j);

theorem :: GOBOARD6:86
   1 <= i & i+1 <= len G implies
  LSeg(p,1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|)
     meets Int cell(G,i,width G);

theorem :: GOBOARD6:87
   1 <= i & i+1 <= len G implies
  LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,p) meets Int cell(G,i,0);

theorem :: GOBOARD6:88
   1 <= j & j+1 <= width G implies
  LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,p) meets Int cell(G,0,j);

theorem :: GOBOARD6:89
   1 <= j & j+1 <= width G implies
  LSeg(p,1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|) meets Int cell(G,len G,j);

theorem :: GOBOARD6:90
    LSeg(p,G*(1,1)-|[1,1]|) meets Int cell(G,0,0);

theorem :: GOBOARD6:91
    LSeg(p,G*(len G,width G)+|[1,1]|) meets Int cell(G,len G,width G);

theorem :: GOBOARD6:92
    LSeg(p,G*(1,width G)+|[-1,1]|) meets Int cell(G,0,width G);

theorem :: GOBOARD6:93
    LSeg(p,G*(len G,1)+|[1,-1]|) meets Int cell(G,len G,0);