:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 1995
:: Copyright (c) 1995 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 & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of 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 Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of 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 (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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: GOBOARD8:25

for f being non constant standard special_circular_sequence
for i being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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;