:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

theorem :: GOBOARD8:1
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 1 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 1),j) &amp; f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) &amp; 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
proofend;

theorem :: GOBOARD8:2
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) &amp; f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) &amp; 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
proofend;

theorem :: GOBOARD8:3
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) &amp; f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) &amp; 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
proofend;

theorem :: GOBOARD8:4
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 1 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * (i,(j + 1)) &amp; ( ( f /. k = (GoB f) * (i,j) &amp; f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) &amp; 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
proofend;

theorem :: GOBOARD8:5
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * (i,(j + 1)) &amp; f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) &amp; 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
proofend;

theorem :: GOBOARD8:6
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * (i,(j + 1)) &amp; f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) &amp; 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
proofend;

theorem :: GOBOARD8:7
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),1) &amp; ( ( f /. k = (GoB f) * ((i + 2),1) &amp; f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),1) &amp; 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
proofend;

theorem :: GOBOARD8:8
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),1) &amp; ( ( f /. k = (GoB f) * (i,1) &amp; f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) &amp; 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
proofend;

theorem :: GOBOARD8:9
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) &amp; ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) &amp; f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) &amp; 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
proofend;

theorem :: GOBOARD8:10
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i being Element of NAT st 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) &amp; ( ( f /. k = (GoB f) * (i,(width (GoB f))) &amp; f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(width (GoB f))) &amp; 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
proofend;

theorem :: GOBOARD8:11
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for i, j being Element of NAT st 1 <= j &amp; j + 1 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * (i,(j + 1)) &amp; f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) &amp; 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
proofend;

theorem :: GOBOARD8:12
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) &amp; f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) &amp; 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
proofend;

theorem :: GOBOARD8:13
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) &amp; f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) &amp; 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
proofend;

theorem :: GOBOARD8:14
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j &amp; j + 1 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),j) &amp; ( ( f /. k = (GoB f) * (i,j) &amp; f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) &amp; 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
proofend;

theorem :: GOBOARD8:15
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 1),j) &amp; f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) &amp; 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
proofend;

theorem :: GOBOARD8:16
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; 1 <= i &amp; i + 2 <= len (GoB f) &amp; f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((i + 1),j) &amp; f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) &amp; 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
proofend;

theorem :: GOBOARD8:17
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * (1,(j + 1)) &amp; ( ( f /. k = (GoB f) * (1,(j + 2)) &amp; f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) &amp; 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
proofend;

theorem :: GOBOARD8:18
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * (1,(j + 1)) &amp; ( ( f /. k = (GoB f) * (1,j) &amp; f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,j) &amp; 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
proofend;

theorem :: GOBOARD8:19
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) &amp; f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) &amp; 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
proofend;

theorem :: GOBOARD8:20
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k &amp; k + 2 <= len f holds
for j being Element of NAT st 1 <= j &amp; j + 2 <= width (GoB f) &amp; f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) &amp; ( ( f /. k = (GoB f) * ((len (GoB f)),j) &amp; f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) &amp; 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
proofend;

theorem Th21: :: GOBOARD8:21
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ) holds
P misses L~ f
proofend;

theorem Th22: :: GOBOARD8:22
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) holds
P misses L~ f
proofend;

theorem Th23: :: GOBOARD8:23
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ) holds
P misses L~ f
proofend;

theorem Th24: :: GOBOARD8:24
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) holds
P misses L~ f
proofend;

theorem :: GOBOARD8:25
for f being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i &amp; 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
proofend;

theorem :: GOBOARD8:26
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) misses L~ f
proofend;

theorem :: GOBOARD8:27
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:28
for f being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i &amp; 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
proofend;

theorem :: GOBOARD8:29
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:30
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:31
for f being non constant standard special_circular_sequence
for j being Element of NAT st 1 <= j &amp; 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
proofend;

theorem :: GOBOARD8:32
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f
proofend;

theorem :: GOBOARD8:33
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:34
for f being non constant standard special_circular_sequence
for j being Element of NAT st 1 <= j &amp; 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
proofend;

theorem :: GOBOARD8:35
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:36
for f being non constant standard special_circular_sequence holds 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
proofend;

theorem :: GOBOARD8:37
for k being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= k &amp; k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f
proofend;

theorem :: GOBOARD8:38
for k being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= k &amp; k + 1 <= len f holds
Int (right_cell (f,k)) misses L~ f
proofend;