Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### More on Segments on a Go-Board

**by****Andrzej Trybulec**- Received October 17, 1995
- MML identifier: GOBOARD8

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, EUCLID, SEQM_3, GOBOARD5, FINSEQ_1, GOBOARD2, TREES_1, TOPREAL1, ARYTM_3, BOOLE, TOPS_1, ARYTM_1, MCART_1, GOBOARD1, RELAT_1, MATRIX_1, ABSVALUE, FINSEQ_4; notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, BINARITH, FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, PRE_TOPC, TOPS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5; constructors TOPS_1, GROUP_1, GOBOARD5, GOBOARD2, SEQM_3, REAL_1, BINARITH, FINSEQ_4, MEMBERED; clusters STRUCT_0, GOBOARD5, RELSET_1, GOBOARD2, EUCLID, ARYTM_3, MEMBERED; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve i,j,k,i1,j1 for Nat, p for Point of TOP-REAL 2, x for set; reserve f for non constant standard special_circular_sequence; theorem :: GOBOARD8:1 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f & 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f; theorem :: GOBOARD8:2 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f & 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k = (GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f; theorem :: GOBOARD8:3 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f & 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k = (GoB f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f; theorem :: GOBOARD8:4 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f & 1 <= j & j+2 <= width GoB 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+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f; theorem :: GOBOARD8:5 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f & 1 <= j & j+2 <= width GoB 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+2) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f; theorem :: GOBOARD8:6 for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f & 1 <= j & j+2 <= width GoB 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+2) = (GoB f)*(i,j+1) & f/.k = (GoB f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f; theorem :: GOBOARD8:7 for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i+2,1) & f/.(k+2) = (GoB f)*(i+1,2) or f/.(k+2) = (GoB f)*(i+2,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,2))) misses L~f; theorem :: GOBOARD8:8 for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i,1) & f/.(k+2) = (GoB f)*(i+1,2) or f/.(k+2) = (GoB f)*(i,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,2))) misses L~f; theorem :: GOBOARD8:9 for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i+2,width GoB f) & f/.(k+2) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i+2,width GoB f) & f/.k = (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i,width GoB f -' 1)+(GoB f)*(i+1,width GoB f)), 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|) misses L~f; theorem :: GOBOARD8:10 for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i,width GoB f) & f/.(k+2) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i,width GoB f) & f/.k = (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i+1,width GoB f -' 1)+(GoB f)*(i+2,width GoB f)), 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|) misses L~f; theorem :: GOBOARD8:11 for k st 1 <= k & k+2 <= len f for i,j st 1 <= j & j+1 <= width GoB f & 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f; theorem :: GOBOARD8:12 for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f & 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+1,j+2) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k = (GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f; theorem :: GOBOARD8:13 for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f & 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+1,j+2) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k = (GoB f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f; theorem :: GOBOARD8:14 for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+1 <= width GoB f & 1 <= i & i+2 <= len GoB 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+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i+2,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f; theorem :: GOBOARD8:15 for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f & 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f; theorem :: GOBOARD8:16 for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f & 1 <= i & i+2 <= len GoB 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+2) = (GoB f)*(i+1,j) & f/.k = (GoB f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f; theorem :: GOBOARD8:17 for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j+2) & f/.(k+2) = (GoB f)*(2,j+1) or f/.(k+2) = (GoB f)*(1,j+2) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j)+(GoB f)*(2,j+1))) misses L~f; theorem :: GOBOARD8:18 for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j) & f/.(k+2) = (GoB f)*(2,j+1) or f/.(k+2) = (GoB f)*(1,j) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(2,j+2))) misses L~f; theorem :: GOBOARD8:19 for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j+2) & f/.(k+2) = (GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j+2) & f/.k = (GoB f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j)+(GoB f)*(len GoB f,j+1)), 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|) misses L~f; theorem :: GOBOARD8:20 for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j) & f/.(k+2) = (GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j) & f/.k = (GoB f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j+1)+(GoB f)*(len GoB f,j+2)), 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|) misses L~f; reserve P for Subset of TOP-REAL 2; theorem :: GOBOARD8:21 (for p st p in P holds p`1 < (GoB f)*(1,1)`1) implies P misses L~f; theorem :: GOBOARD8:22 (for p st p in P holds p`1 > (GoB f)*(len GoB f,1)`1) implies P misses L~f; theorem :: GOBOARD8:23 (for p st p in P holds p`2 < (GoB f)*(1,1)`2) implies P misses L~f; theorem :: GOBOARD8:24 (for p st p in P holds p`2 > (GoB f)*(1,width GoB f)`2) implies P misses L~f; theorem :: GOBOARD8:25 for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|) misses L~f; theorem :: GOBOARD8:26 LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|) misses L~f; theorem :: GOBOARD8:27 LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|, (GoB f)*(len GoB f,1)+|[1,-1]|) misses L~f; theorem :: GOBOARD8:28 for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|, 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width GoB f))+|[0,1]|) misses L~f; theorem :: GOBOARD8:29 LSeg((GoB f)*(1,width GoB f)+|[-1,1]|, 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(2,width GoB f))+|[0,1]|) misses L~f; theorem :: GOBOARD8:30 LSeg(1/2*((GoB f)*(len GoB f -' 1,width GoB f)+ (GoB f)*(len GoB f,width GoB f))+|[0,1]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f; theorem :: GOBOARD8:31 for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|) misses L~f; theorem :: GOBOARD8:32 LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|) misses L~f; theorem :: GOBOARD8:33 LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))- |[1,0]|, (GoB f)*(1,width GoB f)+|[-1,1]|) misses L~f; theorem :: GOBOARD8:34 for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|, 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|) misses L~f; theorem :: GOBOARD8:35 LSeg((GoB f)*(len GoB f,1)+|[1,-1]|, 1/2*((GoB f)*(len GoB f,1)+(GoB f)*(len GoB f,2))+|[1,0]|) misses L~f; theorem :: GOBOARD8:36 LSeg(1/2*((GoB f)*(len GoB f,width GoB f -' 1)+ (GoB f)*(len GoB f,width GoB f))+|[1,0]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f; theorem :: GOBOARD8:37 1 <= k & k+1 <= len f implies Int left_cell(f,k) misses L~f; theorem :: GOBOARD8:38 1 <= k & k+1 <= len f implies Int right_cell(f,k) misses L~f;

Back to top