:: GOBOARD8 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: GOBOARD8:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem :: GOBOARD8:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
f being
standard non
constant 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
theorem Th21: :: GOBOARD8:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: GOBOARD8:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: GOBOARD8:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: GOBOARD8:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GOBOARD8:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 