:: More on Segments on a Go Board :: by Andrzej Trybulec :: :: Received October 17, 1995 :: Copyright (c) 1995-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, GOBOARD5, XXREAL_0, ARYTM_3, FINSEQ_1, GOBOARD2, TREES_1, PARTFUN1, RELAT_1, RLTOPSP1, XBOOLE_0, TOPREAL1, TARSKI, TOPS_1, ARYTM_1, CARD_1, MCART_1, GOBOARD1, MATRIX_1, NAT_1, COMPLEX1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, NAT_D, PARTFUN1, FINSEQ_1, MATRIX_0, SEQM_3, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, XXREAL_0; constructors REAL_1, NAT_D, TOPS_1, GOBOARD2, GOBOARD5, GOBOARD1, RELSET_1; registrations RELSET_1, XREAL_0, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, NAT_1; 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;