Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### 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));

Back to top