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

theorem :: GOBOARD8:1
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:2
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:3
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:4
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:5
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:6
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:7
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat 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
proof end;

theorem :: GOBOARD8:8
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat 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
proof end;

theorem :: GOBOARD8:9
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat 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
proof end;

theorem :: GOBOARD8:10
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat 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
proof end;

theorem :: GOBOARD8:11
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat 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
proof end;

theorem :: GOBOARD8:12
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat 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
proof end;

theorem :: GOBOARD8:13
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat 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
proof end;

theorem :: GOBOARD8:14
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat 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
proof end;

theorem :: GOBOARD8:15
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat 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
proof end;

theorem :: GOBOARD8:16
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat 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
proof end;

theorem :: GOBOARD8:17
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat 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
proof end;

theorem :: GOBOARD8:18
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat 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
proof end;

theorem :: GOBOARD8:19
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat 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
proof end;

theorem :: GOBOARD8:20
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat 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
proof end;

theorem Th21: :: GOBOARD8:21
for f being non constant standard special_circular_sequence
for P being Subset of () st ( for p being Point of () st p in P holds
p 1 < ((GoB f) * (1,1)) 1 ) holds
P misses L~ f
proof end;

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

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

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

theorem :: GOBOARD8:25
for f being non constant standard special_circular_sequence
for i being Nat 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
proof end;

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
proof end;

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
proof end;

theorem :: GOBOARD8:28
for f being non constant standard special_circular_sequence
for i being Nat 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
proof end;

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
proof end;

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
proof end;

theorem :: GOBOARD8:31
for f being non constant standard special_circular_sequence
for j being Nat 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
proof end;

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
proof end;

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
proof end;

theorem :: GOBOARD8:34
for f being non constant standard special_circular_sequence
for j being Nat 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
proof end;

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
proof end;

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
proof end;

theorem :: GOBOARD8:37
for k being Nat
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f
proof end;

theorem :: GOBOARD8:38
for k being Nat
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) misses L~ f
proof end;