The abstract of the Mizar article:

Introduction to Go-Board --- Part II

by

Jaroslaw Kotowicz, and

Yatsuka Nakamura

Received August 24, 1992

MML identifier: GOBOARD2

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, FINSEQ_1, GOBOARD1, RELAT_1, FUNCT_1, FINSET_1,
      BOOLE, CARD_1, SEQ_2, SEQ_4, LATTICES, ARYTM_1, SQUARE_1, TOPREAL1,
      TARSKI, MCART_1, MATRIX_1, INCSP_1, TREES_1, ORDINAL2, SEQM_3, ABSVALUE,
      GOBOARD2, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, STRUCT_0,
      PRE_TOPC, ABSVALUE, CARD_1, SQUARE_1, SEQ_4, FINSEQ_4, MATRIX_1, EUCLID,
      TOPREAL1, GOBOARD1;
 constructors SEQM_3, REAL_1, NAT_1, ABSVALUE, SQUARE_1, SEQ_4, TOPREAL1,
      GOBOARD1, FINSEQ_4, INT_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, GOBOARD1, FINSET_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0,
      FINSEQ_1, INT_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

 reserve p,p1,p2,q for Point of TOP-REAL 2,
         f,f1,f2,g,g1,g2 for FinSequence of TOP-REAL 2,
         r,s for Real,
         v,v1,v2 for FinSequence of REAL,
         n,m,i,j,k for Nat,
         G for Go-board,
         x for set;

scheme PiLambdaD{D()-> non empty set, l()->Nat, F(set)-> Element of D()}:
 ex g being FinSequence of D() st
  len g=l() & for n st n in dom g holds g/.n=F(n);

:::::::::::::::::::::::::::::
:: Real numbers prelimineries
:::::::::::::::::::::::::::::

theorem :: GOBOARD2:1
 for R being finite Subset of REAL holds
  R <> {} implies R is bounded_above & upper_bound(R) in R &
                             R is bounded_below & lower_bound(R) in R;

begin

canceled;

theorem :: GOBOARD2:3
for f being FinSequence
  holds 1 <= n & n+1 <= len f iff n in dom f & n+1 in dom f;

theorem :: GOBOARD2:4
for f being FinSequence
  holds 1 <= n & n+2 <= len f iff n in dom f & n+1 in dom f & n+2 in dom f;

theorem :: GOBOARD2:5
 for D being non empty set, f1,f2 being FinSequence of D, n
  st 1 <= n & n <= len f2 holds (f1^f2)/.(n + len f1) = f2/.n;

theorem :: GOBOARD2:6
  (for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in dom f
holds
  LSeg(f,n) misses LSeg(f,m)) implies f is s.n.c.;

theorem :: GOBOARD2:7
   f is unfolded s.n.c. one-to-one &
  f/.len f in LSeg(f,i) & i in dom f & i+1 in dom f implies i+1=len f;

theorem :: GOBOARD2:8
k<>0 & len f = k+1 implies L~f = L~(f|k) \/ LSeg(f,k);

theorem :: GOBOARD2:9
   1 < k & len f = k+1 & f is unfolded s.n.c. implies
  L~(f|k) /\ LSeg(f,k) = {f/.k};

theorem :: GOBOARD2:10
  len f1 < n & n+1 <= len (f1^f2) & m+len f1 = n implies
LSeg(f1^f2,n) = LSeg(f2,m);

theorem :: GOBOARD2:11
L~f c= L~(f^g);

theorem :: GOBOARD2:12
   f is s.n.c. implies f|i is s.n.c.;

theorem :: GOBOARD2:13
   f1 is special & f2 is special &
  ((f1/.len f1)`1=(f2/.1)`1 or (f1/.len f1)`2=(f2/.1)`2) implies
     f1^f2 is special;

theorem :: GOBOARD2:14
f <> {} implies X_axis(f) <> {};

theorem :: GOBOARD2:15
f <> {} implies Y_axis(f) <> {};

definition let f be non empty FinSequence of TOP-REAL 2;
 cluster X_axis f -> non empty;
 cluster Y_axis f -> non empty;
end;

theorem :: GOBOARD2:16
 f is special implies
for n st n in dom f & n+1 in dom f holds
 for i,j,m,k st [i,j] in Indices G & [m,k] in Indices G & f/.n=G*(i,j) &
                f/.(n+1)=G*(m,k) holds i=m or k=j;

theorem :: GOBOARD2:17
  (for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) &
 f is special &
 (for n st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1))
 implies
 ex g st g is_sequence_on G & L~f = L~g & g/.1=f/.1 &
        g/.len g=f/.len f & len f<=len g;

theorem :: GOBOARD2:18
  v is increasing implies
for n,m st n in dom v & m in dom v & n<=m holds v.n <= v.m;

theorem :: GOBOARD2:19
v is increasing implies
 for n,m st n in dom v & m in dom v & n<>m holds v.n<>v.m;

theorem :: GOBOARD2:20
v is increasing & v1 = v|Seg n implies v1 is increasing;

theorem :: GOBOARD2:21
 for v holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is increasing;

theorem :: GOBOARD2:22
 for v1,v2 st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing &
  v2 is increasing holds v1 = v2;

begin

::::::::::::::::::::::::
:: Proper text
::::::::::::::::::::::::

definition let v1,v2 be increasing FinSequence of REAL;
 assume  v1 <> {} & v2 <> {};
func GoB(v1,v2) -> Matrix of TOP-REAL 2 means
:: GOBOARD2:def 1
 len it = len v1 & width it = len v2 &
 for n,m st [n,m] in Indices it holds it*(n,m) = |[v1.n,v2.m]|;
end;

definition let v1,v2 be non empty increasing FinSequence of REAL;
 cluster GoB(v1,v2) -> non empty-yielding X_equal-in-line Y_equal-in-column
   Y_increasing-in-line X_increasing-in-column;
end;

definition let v;
func Incr(v) ->increasing FinSequence of REAL means
:: GOBOARD2:def 2
rng it = rng v & len it = card rng v;
end;

definition let f be non empty FinSequence of TOP-REAL 2;
func GoB(f) -> Matrix of TOP-REAL 2 equals
:: GOBOARD2:def 3
 GoB(Incr(X_axis(f)),Incr(Y_axis(f)));
end;

theorem :: GOBOARD2:23
v <> {} implies Incr(v) <> {};

definition let v be non empty FinSequence of REAL;
 cluster Incr v -> non empty;
end;

definition let f be non empty FinSequence of TOP-REAL 2;
 cluster GoB(f) -> non empty-yielding X_equal-in-line Y_equal-in-column
   Y_increasing-in-line X_increasing-in-column;
end;

reserve f for non empty FinSequence of TOP-REAL 2;

theorem :: GOBOARD2:24
 len GoB(f) = card rng X_axis(f) & width GoB(f) = card rng Y_axis(f);

theorem :: GOBOARD2:25
  for n st n in dom f holds
 ex i,j st [i,j] in Indices GoB(f) & f/.n = GoB(f)*(i,j);

theorem :: GOBOARD2:26
   n in dom f &
(for m st m in dom f holds (X_axis(f)).n <= (X_axis(f)).m) implies
f/.n in rng Line(GoB(f),1);

theorem :: GOBOARD2:27
   n in dom f &
(for m st m in dom f holds (X_axis(f)).m <= (X_axis(f)).n) implies
f/.n in rng Line(GoB(f),len GoB(f));

theorem :: GOBOARD2:28
   n in dom f &
(for m st m in dom f holds (Y_axis(f)).n <= (Y_axis(f)).m) implies
f/.n in rng Col(GoB(f),1);

theorem :: GOBOARD2:29
   n in dom f &
(for m st m in dom f holds (Y_axis(f)).m <= (Y_axis(f)).n) implies
f/.n in rng Col(GoB(f),width GoB(f));