:: On the Go Board of a Standard Special Circular Sequence :: by Andrzej Trybulec :: :: Received October 15, 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, XBOOLE_0, FINSEQ_1, EUCLID, REAL_1, PRE_TOPC, GOBOARD1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, SUPINF_2, RLTOPSP1, MCART_1, RELAT_1, TREES_1, SPPOL_1, GOBOARD2, MATRIX_1, PARTFUN1, TOPREAL1, TOPS_1, GOBOARD5, TARSKI, FUNCT_1, FINSET_1, FINSEQ_6, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, NAT_1, INT_2, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSET_1, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, FINSEQ_6, GOBOARD5; constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, INT_2, NAT_D, TOPS_1, GOBOARD2, SPPOL_1, GOBOARD5, GOBOARD1, DOMAIN_1, BINOP_2, RELSET_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, FINSET_1, CARD_1, XREAL_0, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve f for non empty FinSequence of TOP-REAL 2, i,j,k,k1,k2,n,i1,i2,j1,j2 for Nat, r,s,r1,r2 for Real, p,q,p1,q1 for Point of TOP-REAL 2, G for Go-board; theorem :: GOBOARD7:1 |.r1-r2.| > s implies r1+s < r2 or r2+s < r1; theorem :: GOBOARD7:2 |.r-s.| = 0 iff r = s; theorem :: GOBOARD7:3 for p,p1,q being Point of TOP-REAL n st p + p1 = q + p1 holds p = q; theorem :: GOBOARD7:4 for p,p1,q being Point of TOP-REAL n st p1 + p = p1 + q holds p = q; theorem :: GOBOARD7:5 p1 in LSeg(p,q) & p`1 = q`1 implies p1`1 = q`1; theorem :: GOBOARD7:6 p1 in LSeg(p,q) & p`2 = q`2 implies p1`2 = q`2; theorem :: GOBOARD7:7 p`1 = q`1 & q`1 = p1`1 & p`2 <= q`2 & q`2 <= p1`2 implies q in LSeg(p,p1); theorem :: GOBOARD7:8 p`1 <= q`1 & q`1 <= p1`1 & p`2 = q`2 & q`2 = p1`2 implies q in LSeg(p,p1); theorem :: GOBOARD7:9 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies 1/2*(G*(i,j)+G *(i+1,j+1)) = 1/2*(G*(i,j+1)+G*(i+1,j)); theorem :: GOBOARD7:10 LSeg(f,k) is horizontal implies ex j st 1 <= j & j <= width GoB f & for p st p in LSeg(f,k) holds p`2 = (GoB f)*(1,j)`2; theorem :: GOBOARD7:11 LSeg(f,k) is vertical implies ex i st 1 <= i & i <= len GoB f & for p st p in LSeg(f,k) holds p`1 = (GoB f)*(i,1)`1; theorem :: GOBOARD7:12 f is special & i <= len GoB f & j <= width GoB f implies Int cell(GoB f,i,j) misses L~f; begin :: Segments on a Go Board theorem :: GOBOARD7:13 1 <= i & i <= len G & 1 <= j & j+2 <= width G implies LSeg(G*(i, j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2)) = { G*(i,j+1) }; theorem :: GOBOARD7:14 1 <= i & i+2 <= len G & 1 <= j & j <= width G implies LSeg(G*(i, j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j)) = { G*(i+1,j) }; theorem :: GOBOARD7:15 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*( i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1)) = { G*(i,j+1) }; theorem :: GOBOARD7:16 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*( i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G* (i+1,j+1) }; theorem :: GOBOARD7:17 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*( i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G*(i,j+1)) = { G*(i,j) }; theorem :: GOBOARD7:18 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(G*( i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*(i+1,j) }; theorem :: GOBOARD7:19 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) holds i1 = i2 & |.j1-j2.| <= 1; theorem :: GOBOARD7:20 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds j1 = j2 & |.i1-i2.| <= 1; theorem :: GOBOARD7:21 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds (i1 = i2 or i1 = i2+1) & (j1 = j2 or j1+1 = j2); theorem :: GOBOARD7:22 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & LSeg (G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1)) holds j1 = j2 & LSeg( G*(i1,j1),G*(i1,j1+1)) = LSeg(G*(i2,j2),G*(i2,j2+1)) or j1 = j2+1 & LSeg(G*(i1, j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G* (i1,j1) } or j1+1 = j2 & LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G* (i2,j2) }; theorem :: GOBOARD7:23 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg(G *(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds i1 = i2 & LSeg(G* (i1,j1),G*(i1+1,j1)) = LSeg(G*(i2,j2),G*(i2+1,j2)) or i1 = i2+1 & LSeg(G*(i1,j1 ),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1) } or i1+1 = i2 & LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i2,j2) }; theorem :: GOBOARD7:24 for i1,j1,i2,j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2)) holds j1 = j2 & LSeg( G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1) } or j1+1 = j2 & LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G* (i1,j1 +1) }; theorem :: GOBOARD7:25 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & 1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*( i2,j2),G*(i2,j2+1)) implies i1 = i2 & j1 = j2; theorem :: GOBOARD7:26 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 +1 <= len G & 1 <= j2 & j2 <= width G & 1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*( i2,j2),G*(i2+1,j2)) implies i1 = i2 & j1 = j2; theorem :: GOBOARD7:27 1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G implies not ex i2,j2 st 1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G & 1/2*(G*(i1,j1)+G*( i1+1,j1)) in LSeg(G*(i2,j2),G*(i2,j2+1)); theorem :: GOBOARD7:28 1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G implies not ex i2,j2 st 1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G & 1/2*(G*(i1,j1)+G*( i1,j1+1)) in LSeg(G*(i2,j2),G*(i2+1,j2)); begin :: Standard special circular sequences reserve f for non constant standard special_circular_sequence; theorem :: GOBOARD7:29 for f being standard non empty FinSequence of TOP-REAL 2 st i in dom f & i+1 in dom f holds f/.i <> f/.(i+1); theorem :: GOBOARD7:30 ex i st i in dom f & (f/.i)`1 <> (f/.1)`1; theorem :: GOBOARD7:31 ex i st i in dom f & (f/.i)`2 <> (f/.1)`2; theorem :: GOBOARD7:32 len GoB f > 1; theorem :: GOBOARD7:33 width GoB f > 1; theorem :: GOBOARD7:34 len f > 4; theorem :: GOBOARD7:35 for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f > 4 for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j; theorem :: GOBOARD7:36 for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j; theorem :: GOBOARD7:37 for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j; theorem :: GOBOARD7:38 for i being Nat st 1 < i & i <= len f & f/.i = f/.1 holds i = len f; theorem :: GOBOARD7:39 1 <= i & i <= len GoB f & 1 <= j & j+1 <= width GoB f & 1/2*(( GoB f)*(i,j)+(GoB f)*(i,j+1)) in L~f implies ex k st 1 <= k & k+1 <= len f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k); theorem :: GOBOARD7:40 1 <= i & i+1 <= len GoB f & 1 <= j & j <= width GoB f & 1/2*(( GoB f)*(i,j)+(GoB f)*(i+1,j)) in L~f implies ex k st 1 <= k & k+1 <= len f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k); theorem :: GOBOARD7:41 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i +1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+1) & f/.(k+1 ) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i+1,j); theorem :: GOBOARD7:42 1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k) & LSeg((GoB f)*(i,j), (GoB f)*(i,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+2) & f/.(k+1) = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i,j); theorem :: GOBOARD7:43 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i ,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i,j); theorem :: GOBOARD7:44 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i ,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j) & f/.(k+1 ) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j+1); theorem :: GOBOARD7:45 1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k) & LSeg((GoB f)*(i,j), (GoB f)*(i+1,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+2,j) & f/.(k+1) = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j); theorem :: GOBOARD7:46 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i ,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j); theorem :: GOBOARD7:47 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i ,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i+1,j) & f/.(k+1 ) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j+1); theorem :: GOBOARD7:48 1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i,j+1), (GoB f)*(i,j+2)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f )*(i,j+1) & f/.(k+2) = (GoB f)*(i,j+2); theorem :: GOBOARD7:49 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i,j+1 ),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = ( GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j+1); theorem :: GOBOARD7:50 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) & LSeg((GoB f)*(i +1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j+1) & f/.(k+1 ) = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i+1,j); theorem :: GOBOARD7:51 1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) & LSeg((GoB f)*(i+1,j), (GoB f)*(i+2,j)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f )*(i+1,j) & f/.(k+2) = (GoB f)*(i+2,j); theorem :: GOBOARD7:52 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <= k & k+1 < len f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) & LSeg((GoB f)*(i+1,j ),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies f/.k = (GoB f)*(i,j) & f/.(k+1) = ( GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i+1,j+1); theorem :: GOBOARD7:53 1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f implies f/.1 = (GoB f)*(i,j+1) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f )*(i,j+2) or f/.2 = (GoB f)*(i,j+2) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i,j+2) & f/.(k+2) = (GoB f)*(i,j)) ; theorem :: GOBOARD7:54 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg(( GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f implies f/.1 = (GoB f)*(i,j+1) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k = (GoB f)* (i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = ( GoB f)*(i,j)); theorem :: GOBOARD7:55 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg(( GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1, j)) c= L~f implies f/.1 = (GoB f)*(i+1,j+1) & (f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+1,j) or f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i, j+1)) or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i+1,j) & f/.(k+ 2) = (GoB f)*(i,j+1)); theorem :: GOBOARD7:56 1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f implies f/.1 = (GoB f)*(i+1,j) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f )*(i+2,j) or f/.2 = (GoB f)*(i+2,j) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i+2,j) & f/.(k+2) = (GoB f)*(i,j)) ; theorem :: GOBOARD7:57 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg(( GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f implies f/.1 = (GoB f)*(i+1,j) & (f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j)) or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k = (GoB f)* (i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = ( GoB f)*(i,j)); theorem :: GOBOARD7:58 1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & LSeg(( GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i,j+ 1)) c= L~f implies f/.1 = (GoB f)*(i+1,j+1) & (f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,j+1) or f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+ 1,j)) or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i,j+1) & f/.(k+ 2) = (GoB f)*(i+1,j)); theorem :: GOBOARD7:59 1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies not ( LSeg ((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f); theorem :: GOBOARD7:60 1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies not ( LSeg ((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+ 1,j+2)) c= L~f & LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f); theorem :: GOBOARD7:61 1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies not ( LSeg ((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f); theorem :: GOBOARD7:62 1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies not ( LSeg ((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f & LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+ 2,j+1)) c= L~f & LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f); :: Moved from JORDAN15, AK, 22.02.2006 theorem :: GOBOARD7:63 for p,q,p1,q1 be Point of TOP-REAL 2 st LSeg(p,q) is vertical & LSeg( p1,q1) is vertical & p`1 = p1`1 & p`2 <= p1`2 & p1`2 <= q1`2 & q1`2 <= q`2 holds LSeg(p1,q1) c= LSeg(p,q); theorem :: GOBOARD7:64 for p,q,p1,q1 be Point of TOP-REAL 2 st LSeg(p,q) is horizontal & LSeg (p1,q1) is horizontal & p`2 = p1`2 & p`1 <= p1`1 & p1`1 <= q1`1 & q1`1 <= q`1 holds LSeg(p1,q1) c= LSeg(p,q);