The abstract of the Mizar article:

Go-Board Theorem

by

Jaroslaw Kotowicz, and

Yatsuka Nakamura

Received August 24, 1992

MML identifier: GOBOARD4

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, FINSEQ_1, GOBOARD1, FINSEQ_4, RELAT_1, INCSP_1,
      MATRIX_1, TREES_1, BOOLE, FUNCT_1, ARYTM_1, ABSVALUE, MATRIX_2, TOPREAL1,
      GOBOARD2, MCART_1, TOPREAL4, GOBOARD4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, FUNCT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, ABSVALUE, FINSEQ_4,
      MATRIX_1, EUCLID, TOPREAL1, TOPREAL4, GOBOARD1, GOBOARD2;
 constructors REAL_1, NAT_1, ABSVALUE, TOPREAL1, MATRIX_2, TOPREAL4, GOBOARD2,
      FINSEQ_4, INT_1, MEMBERED, XBOOLE_0;
 clusters GOBOARD1, RELSET_1, GOBOARD2, STRUCT_0, EUCLID, INT_1, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

 reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2,
          P1,P2 for Subset of TOP-REAL 2,
          f,f1,f2,g1,g2 for FinSequence of TOP-REAL 2,
          n,m,i,j,k for Nat,
          G,G1 for Go-board,
          x,y for set;

theorem :: GOBOARD4:1
for G,f1,f2 st 1<=len f1 & 1<=len f2 &
 f1 is_sequence_on G & f2 is_sequence_on G &
 f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
 f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
 rng f1 meets rng f2;

theorem :: GOBOARD4:2
for G,f1,f2 st 2<=len f1 & 2<=len f2 &
  f1 is_sequence_on G & f2 is_sequence_on G &
  f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
  f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
L~f1 meets L~f2;

theorem :: GOBOARD4:3
  for G,f1,f2 st 2 <= len f1 & 2 <= len f2 &
  f1 is_sequence_on G & f2 is_sequence_on G &
  f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
  f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds
L~f1 meets L~f2;

definition let f be FinSequence of REAL, r,s be Real;
 pred f lies_between r,s means
:: GOBOARD4:def 1
  for n st n in dom f holds r <= f.n & f.n <= s;
end;

definition let D be non empty set;
 let f1 be FinSequence of D, f2 be non empty FinSequence of D;
 cluster f1^f2 -> non empty;
 cluster f2^f1 -> non empty;
end;

theorem :: GOBOARD4:4
for f1,f2 being FinSequence of TOP-REAL 2 st
 2<=len f1 & 2<=len f2 & f1 is special & f2 is special &
 (for n st n in dom f1 & n+1 in dom f1 holds f1/.n <> f1/.(n+1)) &
 (for n st n in dom f2 & n+1 in dom f2 holds f2/.n <> f2/.(n+1)) &
 X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
 Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
  L~f1 meets L~f2;

theorem :: GOBOARD4:5
for f1,f2 being FinSequence of TOP-REAL 2 st
 f1 is one-to-one special & 2 <= len f1 &
 f2 is one-to-one special & 2 <= len f2 &
 X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
 Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
  L~f1 meets L~f2;

canceled 2;

theorem :: GOBOARD4:8
  for P1,P2,p1,p2,q1,q2 st
   P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 &
   (for p st p in P1 \/ P2 holds p1`1<=p`1 & p`1<=q1`1) &
   (for p st p in P1 \/ P2 holds p2`2<=p`2 & p`2<=q2`2) holds
P1 meets P2;