:: GOBOARD8 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: GOBOARD8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GOBOARD8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th21: :: GOBOARD8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being standard non constant 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for f being standard non constant special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell f,k) misses L~ f
proof end;

theorem :: GOBOARD8:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for f being standard non constant special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) misses L~ f
proof end;