:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 1995
:: Copyright (c) 1995 Association of Mizar Users
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
theorem Th21: :: GOBOARD8:21
theorem Th22: :: GOBOARD8:22
theorem Th23: :: GOBOARD8:23
theorem Th24: :: GOBOARD8:24
theorem :: GOBOARD8:25
theorem :: GOBOARD8:26
theorem :: GOBOARD8:27
theorem :: GOBOARD8:28
theorem :: GOBOARD8:29
theorem :: GOBOARD8:30
theorem :: GOBOARD8:31
theorem :: GOBOARD8:32
theorem :: GOBOARD8:33
theorem :: GOBOARD8:34
theorem :: GOBOARD8:35
theorem :: GOBOARD8:36
theorem :: GOBOARD8:37
theorem :: GOBOARD8:38