:: GOBOARD8 semantic presentation

theorem Th1: :: GOBOARD8:1
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 1 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * (b3 + 1),b4 & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),(b4 + 2) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),b4 & b1 /. b2 = (GoB b1) * (b3 + 1),(b4 + 2) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,b4) + ((GoB b1) * (b3 + 1),(b4 + 1)))),((1 / 2) * (((GoB b1) * b3,(b4 + 1)) + ((GoB b1) * (b3 + 1),(b4 + 2)))) misses L~ b1
proof end;

theorem Th2: :: GOBOARD8:2
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * (b3 + 2),(b4 + 1) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),(b4 + 2) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b3 + 2),(b4 + 1) & b1 /. b2 = (GoB b1) * (b3 + 1),(b4 + 2) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,b4) + ((GoB b1) * (b3 + 1),(b4 + 1)))),((1 / 2) * (((GoB b1) * b3,(b4 + 1)) + ((GoB b1) * (b3 + 1),(b4 + 2)))) misses L~ b1
proof end;

theorem Th3: :: GOBOARD8:3
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * (b3 + 2),(b4 + 1) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),b4 ) or ( b1 /. (b2 + 2) = (GoB b1) * (b3 + 2),(b4 + 1) & b1 /. b2 = (GoB b1) * (b3 + 1),b4 ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,b4) + ((GoB b1) * (b3 + 1),(b4 + 1)))),((1 / 2) * (((GoB b1) * b3,(b4 + 1)) + ((GoB b1) * (b3 + 1),(b4 + 2)))) misses L~ b1
proof end;

theorem Th4: :: GOBOARD8:4
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 1 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * b3,(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * b3,b4 & b1 /. (b2 + 2) = (GoB b1) * b3,(b4 + 2) ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,b4 & b1 /. b2 = (GoB b1) * b3,(b4 + 2) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,b4) + ((GoB b1) * (b3 + 1),(b4 + 1)))),((1 / 2) * (((GoB b1) * b3,(b4 + 1)) + ((GoB b1) * (b3 + 1),(b4 + 2)))) misses L~ b1
proof end;

theorem Th5: :: GOBOARD8:5
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * b3,(b4 + 1) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),(b4 + 2) ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,(b4 + 1) & b1 /. b2 = (GoB b1) * (b3 + 1),(b4 + 2) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * (b3 + 1),b4) + ((GoB b1) * (b3 + 2),(b4 + 1)))),((1 / 2) * (((GoB b1) * (b3 + 1),(b4 + 1)) + ((GoB b1) * (b3 + 2),(b4 + 2)))) misses L~ b1
proof end;

theorem Th6: :: GOBOARD8:6
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & 1 <= b4 & b4 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * b3,(b4 + 1) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),b4 ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,(b4 + 1) & b1 /. b2 = (GoB b1) * (b3 + 1),b4 ) ) holds
LSeg ((1 / 2) * (((GoB b1) * (b3 + 1),b4) + ((GoB b1) * (b3 + 2),(b4 + 1)))),((1 / 2) * (((GoB b1) * (b3 + 1),(b4 + 1)) + ((GoB b1) * (b3 + 2),(b4 + 2)))) misses L~ b1
proof end;

theorem Th7: :: GOBOARD8:7
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),1 & ( ( b1 /. b2 = (GoB b1) * (b3 + 2),1 & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),2 ) or ( b1 /. (b2 + 2) = (GoB b1) * (b3 + 2),1 & b1 /. b2 = (GoB b1) * (b3 + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB b1) * b3,1) + ((GoB b1) * (b3 + 1),1))) - |[0,1]|),((1 / 2) * (((GoB b1) * b3,1) + ((GoB b1) * (b3 + 1),2))) misses L~ b1
proof end;

theorem Th8: :: GOBOARD8:8
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),1 & ( ( b1 /. b2 = (GoB b1) * b3,1 & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),2 ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,1 & b1 /. b2 = (GoB b1) * (b3 + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB b1) * (b3 + 1),1) + ((GoB b1) * (b3 + 2),1))) - |[0,1]|),((1 / 2) * (((GoB b1) * (b3 + 1),1) + ((GoB b1) * (b3 + 2),2))) misses L~ b1
proof end;

theorem Th9: :: GOBOARD8:9
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(width (GoB b1)) & ( ( b1 /. b2 = (GoB b1) * (b3 + 2),(width (GoB b1)) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),((width (GoB b1)) -' 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b3 + 2),(width (GoB b1)) & b1 /. b2 = (GoB b1) * (b3 + 1),((width (GoB b1)) -' 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,((width (GoB b1)) -' 1)) + ((GoB b1) * (b3 + 1),(width (GoB b1))))),(((1 / 2) * (((GoB b1) * b3,(width (GoB b1))) + ((GoB b1) * (b3 + 1),(width (GoB b1))))) + |[0,1]|) misses L~ b1
proof end;

theorem Th10: :: GOBOARD8:10
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(width (GoB b1)) & ( ( b1 /. b2 = (GoB b1) * b3,(width (GoB b1)) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 1),((width (GoB b1)) -' 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,(width (GoB b1)) & b1 /. b2 = (GoB b1) * (b3 + 1),((width (GoB b1)) -' 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * (b3 + 1),((width (GoB b1)) -' 1)) + ((GoB b1) * (b3 + 2),(width (GoB b1))))),(((1 / 2) * (((GoB b1) * (b3 + 1),(width (GoB b1))) + ((GoB b1) * (b3 + 2),(width (GoB b1))))) + |[0,1]|) misses L~ b1
proof end;

theorem Th11: :: GOBOARD8:11
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b4 & b4 + 1 <= width (GoB b1) & 1 <= b3 & b3 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b3 + 1),(b4 + 1) & ( ( b1 /. b2 = (GoB b1) * b3,(b4 + 1) & b1 /. (b2 + 2) = (GoB b1) * (b3 + 2),(b4 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * b3,(b4 + 1) & b1 /. b2 = (GoB b1) * (b3 + 2),(b4 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b3,b4) + ((GoB b1) * (b3 + 1),(b4 + 1)))),((1 / 2) * (((GoB b1) * (b3 + 1),b4) + ((GoB b1) * (b3 + 2),(b4 + 1)))) misses L~ b1
proof end;

theorem Th12: :: GOBOARD8:12
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & 1 <= b4 & b4 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b4 + 1),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (b4 + 1),(b3 + 2) & b1 /. (b2 + 2) = (GoB b1) * (b4 + 2),(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b4 + 1),(b3 + 2) & b1 /. b2 = (GoB b1) * (b4 + 2),(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b4,b3) + ((GoB b1) * (b4 + 1),(b3 + 1)))),((1 / 2) * (((GoB b1) * (b4 + 1),b3) + ((GoB b1) * (b4 + 2),(b3 + 1)))) misses L~ b1
proof end;

theorem Th13: :: GOBOARD8:13
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & 1 <= b4 & b4 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b4 + 1),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (b4 + 1),(b3 + 2) & b1 /. (b2 + 2) = (GoB b1) * b4,(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b4 + 1),(b3 + 2) & b1 /. b2 = (GoB b1) * b4,(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b4,b3) + ((GoB b1) * (b4 + 1),(b3 + 1)))),((1 / 2) * (((GoB b1) * (b4 + 1),b3) + ((GoB b1) * (b4 + 2),(b3 + 1)))) misses L~ b1
proof end;

theorem Th14: :: GOBOARD8:14
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 1 <= width (GoB b1) & 1 <= b4 & b4 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b4 + 1),b3 & ( ( b1 /. b2 = (GoB b1) * b4,b3 & b1 /. (b2 + 2) = (GoB b1) * (b4 + 2),b3 ) or ( b1 /. (b2 + 2) = (GoB b1) * b4,b3 & b1 /. b2 = (GoB b1) * (b4 + 2),b3 ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b4,b3) + ((GoB b1) * (b4 + 1),(b3 + 1)))),((1 / 2) * (((GoB b1) * (b4 + 1),b3) + ((GoB b1) * (b4 + 2),(b3 + 1)))) misses L~ b1
proof end;

theorem Th15: :: GOBOARD8:15
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & 1 <= b4 & b4 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b4 + 1),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (b4 + 1),b3 & b1 /. (b2 + 2) = (GoB b1) * (b4 + 2),(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b4 + 1),b3 & b1 /. b2 = (GoB b1) * (b4 + 2),(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b4,(b3 + 1)) + ((GoB b1) * (b4 + 1),(b3 + 2)))),((1 / 2) * (((GoB b1) * (b4 + 1),(b3 + 1)) + ((GoB b1) * (b4 + 2),(b3 + 2)))) misses L~ b1
proof end;

theorem Th16: :: GOBOARD8:16
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & 1 <= b4 & b4 + 2 <= len (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (b4 + 1),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (b4 + 1),b3 & b1 /. (b2 + 2) = (GoB b1) * b4,(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (b4 + 1),b3 & b1 /. b2 = (GoB b1) * b4,(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * b4,(b3 + 1)) + ((GoB b1) * (b4 + 1),(b3 + 2)))),((1 / 2) * (((GoB b1) * (b4 + 1),(b3 + 1)) + ((GoB b1) * (b4 + 2),(b3 + 2)))) misses L~ b1
proof end;

theorem Th17: :: GOBOARD8:17
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * 1,(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * 1,(b3 + 2) & b1 /. (b2 + 2) = (GoB b1) * 2,(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * 1,(b3 + 2) & b1 /. b2 = (GoB b1) * 2,(b3 + 1) ) ) holds
LSeg (((1 / 2) * (((GoB b1) * 1,b3) + ((GoB b1) * 1,(b3 + 1)))) - |[1,0]|),((1 / 2) * (((GoB b1) * 1,b3) + ((GoB b1) * 2,(b3 + 1)))) misses L~ b1
proof end;

theorem Th18: :: GOBOARD8:18
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * 1,(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * 1,b3 & b1 /. (b2 + 2) = (GoB b1) * 2,(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * 1,b3 & b1 /. b2 = (GoB b1) * 2,(b3 + 1) ) ) holds
LSeg (((1 / 2) * (((GoB b1) * 1,(b3 + 1)) + ((GoB b1) * 1,(b3 + 2)))) - |[1,0]|),((1 / 2) * (((GoB b1) * 1,(b3 + 1)) + ((GoB b1) * 2,(b3 + 2)))) misses L~ b1
proof end;

theorem Th19: :: GOBOARD8:19
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (len (GoB b1)),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (len (GoB b1)),(b3 + 2) & b1 /. (b2 + 2) = (GoB b1) * ((len (GoB b1)) -' 1),(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (len (GoB b1)),(b3 + 2) & b1 /. b2 = (GoB b1) * ((len (GoB b1)) -' 1),(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * ((len (GoB b1)) -' 1),b3) + ((GoB b1) * (len (GoB b1)),(b3 + 1)))),(((1 / 2) * (((GoB b1) * (len (GoB b1)),b3) + ((GoB b1) * (len (GoB b1)),(b3 + 1)))) + |[1,0]|) misses L~ b1
proof end;

theorem Th20: :: GOBOARD8:20
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
for b3 being Nat st 1 <= b3 & b3 + 2 <= width (GoB b1) & b1 /. (b2 + 1) = (GoB b1) * (len (GoB b1)),(b3 + 1) & ( ( b1 /. b2 = (GoB b1) * (len (GoB b1)),b3 & b1 /. (b2 + 2) = (GoB b1) * ((len (GoB b1)) -' 1),(b3 + 1) ) or ( b1 /. (b2 + 2) = (GoB b1) * (len (GoB b1)),b3 & b1 /. b2 = (GoB b1) * ((len (GoB b1)) -' 1),(b3 + 1) ) ) holds
LSeg ((1 / 2) * (((GoB b1) * ((len (GoB b1)) -' 1),(b3 + 1)) + ((GoB b1) * (len (GoB b1)),(b3 + 2)))),(((1 / 2) * (((GoB b1) * (len (GoB b1)),(b3 + 1)) + ((GoB b1) * (len (GoB b1)),(b3 + 2)))) + |[1,0]|) misses L~ b1
proof end;

theorem Th21: :: GOBOARD8:21
for b1 being standard non constant special_circular_sequence
for b2 being Subset of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) st b3 in b2 holds
b3 `1 < ((GoB b1) * 1,1) `1 ) holds
b2 misses L~ b1
proof end;

theorem Th22: :: GOBOARD8:22
for b1 being standard non constant special_circular_sequence
for b2 being Subset of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) st b3 in b2 holds
b3 `1 > ((GoB b1) * (len (GoB b1)),1) `1 ) holds
b2 misses L~ b1
proof end;

theorem Th23: :: GOBOARD8:23
for b1 being standard non constant special_circular_sequence
for b2 being Subset of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) st b3 in b2 holds
b3 `2 < ((GoB b1) * 1,1) `2 ) holds
b2 misses L~ b1
proof end;

theorem Th24: :: GOBOARD8:24
for b1 being standard non constant special_circular_sequence
for b2 being Subset of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) st b3 in b2 holds
b3 `2 > ((GoB b1) * 1,(width (GoB b1))) `2 ) holds
b2 misses L~ b1
proof end;

theorem Th25: :: GOBOARD8:25
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len (GoB b1) holds
LSeg (((1 / 2) * (((GoB b1) * b2,1) + ((GoB b1) * (b2 + 1),1))) - |[0,1]|),(((1 / 2) * (((GoB b1) * (b2 + 1),1) + ((GoB b1) * (b2 + 2),1))) - |[0,1]|) misses L~ b1
proof end;

theorem Th26: :: GOBOARD8:26
for b1 being standard non constant special_circular_sequence holds LSeg (((GoB b1) * 1,1) - |[1,1]|),(((1 / 2) * (((GoB b1) * 1,1) + ((GoB b1) * 2,1))) - |[0,1]|) misses L~ b1
proof end;

theorem Th27: :: GOBOARD8:27
for b1 being standard non constant special_circular_sequence holds LSeg (((1 / 2) * (((GoB b1) * ((len (GoB b1)) -' 1),1) + ((GoB b1) * (len (GoB b1)),1))) - |[0,1]|),(((GoB b1) * (len (GoB b1)),1) + |[1,(- 1)]|) misses L~ b1
proof end;

theorem Th28: :: GOBOARD8:28
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= len (GoB b1) holds
LSeg (((1 / 2) * (((GoB b1) * b2,(width (GoB b1))) + ((GoB b1) * (b2 + 1),(width (GoB b1))))) + |[0,1]|),(((1 / 2) * (((GoB b1) * (b2 + 1),(width (GoB b1))) + ((GoB b1) * (b2 + 2),(width (GoB b1))))) + |[0,1]|) misses L~ b1
proof end;

theorem Th29: :: GOBOARD8:29
for b1 being standard non constant special_circular_sequence holds LSeg (((GoB b1) * 1,(width (GoB b1))) + |[(- 1),1]|),(((1 / 2) * (((GoB b1) * 1,(width (GoB b1))) + ((GoB b1) * 2,(width (GoB b1))))) + |[0,1]|) misses L~ b1
proof end;

theorem Th30: :: GOBOARD8:30
for b1 being standard non constant special_circular_sequence holds LSeg (((1 / 2) * (((GoB b1) * ((len (GoB b1)) -' 1),(width (GoB b1))) + ((GoB b1) * (len (GoB b1)),(width (GoB b1))))) + |[0,1]|),(((GoB b1) * (len (GoB b1)),(width (GoB b1))) + |[1,1]|) misses L~ b1
proof end;

theorem Th31: :: GOBOARD8:31
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= width (GoB b1) holds
LSeg (((1 / 2) * (((GoB b1) * 1,b2) + ((GoB b1) * 1,(b2 + 1)))) - |[1,0]|),(((1 / 2) * (((GoB b1) * 1,(b2 + 1)) + ((GoB b1) * 1,(b2 + 2)))) - |[1,0]|) misses L~ b1
proof end;

theorem Th32: :: GOBOARD8:32
for b1 being standard non constant special_circular_sequence holds LSeg (((GoB b1) * 1,1) - |[1,1]|),(((1 / 2) * (((GoB b1) * 1,1) + ((GoB b1) * 1,2))) - |[1,0]|) misses L~ b1
proof end;

theorem Th33: :: GOBOARD8:33
for b1 being standard non constant special_circular_sequence holds LSeg (((1 / 2) * (((GoB b1) * 1,((width (GoB b1)) -' 1)) + ((GoB b1) * 1,(width (GoB b1))))) - |[1,0]|),(((GoB b1) * 1,(width (GoB b1))) + |[(- 1),1]|) misses L~ b1
proof end;

theorem Th34: :: GOBOARD8:34
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 2 <= width (GoB b1) holds
LSeg (((1 / 2) * (((GoB b1) * (len (GoB b1)),b2) + ((GoB b1) * (len (GoB b1)),(b2 + 1)))) + |[1,0]|),(((1 / 2) * (((GoB b1) * (len (GoB b1)),(b2 + 1)) + ((GoB b1) * (len (GoB b1)),(b2 + 2)))) + |[1,0]|) misses L~ b1
proof end;

theorem Th35: :: GOBOARD8:35
for b1 being standard non constant special_circular_sequence holds LSeg (((GoB b1) * (len (GoB b1)),1) + |[1,(- 1)]|),(((1 / 2) * (((GoB b1) * (len (GoB b1)),1) + ((GoB b1) * (len (GoB b1)),2))) + |[1,0]|) misses L~ b1
proof end;

theorem Th36: :: GOBOARD8:36
for b1 being standard non constant special_circular_sequence holds LSeg (((1 / 2) * (((GoB b1) * (len (GoB b1)),((width (GoB b1)) -' 1)) + ((GoB b1) * (len (GoB b1)),(width (GoB b1))))) + |[1,0]|),(((GoB b1) * (len (GoB b1)),(width (GoB b1))) + |[1,1]|) misses L~ b1
proof end;

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

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