:: GOBOARD7 semantic presentation

theorem Th1: :: GOBOARD7:1
for b1, b2, b3 being Real holds
( not abs (b1 - b2) > b3 or b1 + b3 < b2 or b2 + b3 < b1 )
proof end;

theorem Th2: :: GOBOARD7:2
for b1, b2 being Real holds
( abs (b1 - b2) = 0 iff b1 = b2 )
proof end;

theorem Th3: :: GOBOARD7:3
for b1 being Nat
for b2, b3, b4 being Point of (TOP-REAL b1) st b2 + b3 = b4 + b3 holds
b2 = b4
proof end;

theorem Th4: :: GOBOARD7:4
for b1 being Nat
for b2, b3, b4 being Point of (TOP-REAL b1) st b3 + b2 = b3 + b4 holds
b2 = b4 by Th3;

theorem Th5: :: GOBOARD7:5
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 in LSeg b2,b3 & b2 `1 = b3 `1 holds
b1 `1 = b3 `1
proof end;

theorem Th6: :: GOBOARD7:6
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 in LSeg b2,b3 & b2 `2 = b3 `2 holds
b1 `2 = b3 `2
proof end;

theorem Th7: :: GOBOARD7:7
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1) holds (1 / 2) * (b2 + b3) in LSeg b2,b3
proof end;

theorem Th8: :: GOBOARD7:8
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 `1 = b2 `1 & b2 `1 = b3 `1 & b1 `2 <= b2 `2 & b2 `2 <= b3 `2 holds
b2 in LSeg b1,b3
proof end;

theorem Th9: :: GOBOARD7:9
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 `1 <= b2 `1 & b2 `1 <= b3 `1 & b1 `2 = b2 `2 & b2 `2 = b3 `2 holds
b2 in LSeg b1,b3
proof end;

theorem Th10: :: GOBOARD7:10
for b1 being non empty set
for b2, b3 being Nat
for b4 being Matrix of b1 st 1 <= b2 & b2 <= len b4 & 1 <= b3 & b3 <= width b4 holds
[b2,b3] in Indices b4
proof end;

theorem Th11: :: GOBOARD7:11
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1))) = (1 / 2) * ((b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),b2))
proof end;

theorem Th12: :: GOBOARD7:12
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Nat st LSeg b1,b2 is horizontal holds
ex b3 being Nat st
( 1 <= b3 & b3 <= width (GoB b1) & ( for b4 being Point of (TOP-REAL 2) st b4 in LSeg b1,b2 holds
b4 `2 = ((GoB b1) * 1,b3) `2 ) )
proof end;

theorem Th13: :: GOBOARD7:13
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Nat st LSeg b1,b2 is vertical holds
ex b3 being Nat st
( 1 <= b3 & b3 <= len (GoB b1) & ( for b4 being Point of (TOP-REAL 2) st b4 in LSeg b1,b2 holds
b4 `1 = ((GoB b1) * b3,1) `1 ) )
proof end;

theorem Th14: :: GOBOARD7:14
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Nat st b1 is special & b2 <= len (GoB b1) & b3 <= width (GoB b1) holds
Int (cell (GoB b1),b2,b3) misses L~ b1
proof end;

theorem Th15: :: GOBOARD7:15
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 <= len b3 & 1 <= b2 & b2 + 2 <= width b3 holds
(LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1))) /\ (LSeg (b3 * b1,(b2 + 1)),(b3 * b1,(b2 + 2))) = {(b3 * b1,(b2 + 1))}
proof end;

theorem Th16: :: GOBOARD7:16
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 2 <= len b3 & 1 <= b2 & b2 <= width b3 holds
(LSeg (b3 * b1,b2),(b3 * (b1 + 1),b2)) /\ (LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 2),b2)) = {(b3 * (b1 + 1),b2)}
proof end;

theorem Th17: :: GOBOARD7:17
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1))) /\ (LSeg (b3 * b1,(b2 + 1)),(b3 * (b1 + 1),(b2 + 1))) = {(b3 * b1,(b2 + 1))}
proof end;

theorem Th18: :: GOBOARD7:18
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(LSeg (b3 * b1,(b2 + 1)),(b3 * (b1 + 1),(b2 + 1))) /\ (LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 1),(b2 + 1))) = {(b3 * (b1 + 1),(b2 + 1))}
proof end;

theorem Th19: :: GOBOARD7:19
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(LSeg (b3 * b1,b2),(b3 * (b1 + 1),b2)) /\ (LSeg (b3 * b1,b2),(b3 * b1,(b2 + 1))) = {(b3 * b1,b2)}
proof end;

theorem Th20: :: GOBOARD7:20
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(LSeg (b3 * b1,b2),(b3 * (b1 + 1),b2)) /\ (LSeg (b3 * (b1 + 1),b2),(b3 * (b1 + 1),(b2 + 1))) = {(b3 * (b1 + 1),b2)}
proof end;

theorem Th21: :: GOBOARD7:21
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 + 1 <= width b1 & 1 <= b4 & b4 <= len b1 & 1 <= b5 & b5 + 1 <= width b1 & LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1)) meets LSeg (b1 * b4,b5),(b1 * b4,(b5 + 1)) holds
( b2 = b4 & abs (b3 - b5) <= 1 )
proof end;

theorem Th22: :: GOBOARD7:22
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 + 1 <= len b1 & 1 <= b3 & b3 <= width b1 & 1 <= b4 & b4 + 1 <= len b1 & 1 <= b5 & b5 <= width b1 & LSeg (b1 * b2,b3),(b1 * (b2 + 1),b3) meets LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5) holds
( b3 = b5 & abs (b2 - b4) <= 1 )
proof end;

theorem Th23: :: GOBOARD7:23
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 + 1 <= width b1 & 1 <= b4 & b4 + 1 <= len b1 & 1 <= b5 & b5 <= width b1 & LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1)) meets LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5) holds
( ( b2 = b4 or b2 = b4 + 1 ) & ( b3 = b5 or b3 + 1 = b5 ) )
proof end;

theorem Th24: :: GOBOARD7:24
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 + 1 <= width b1 & 1 <= b4 & b4 <= len b1 & 1 <= b5 & b5 + 1 <= width b1 & LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1)) meets LSeg (b1 * b4,b5),(b1 * b4,(b5 + 1)) & not ( b3 = b5 & LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1)) = LSeg (b1 * b4,b5),(b1 * b4,(b5 + 1)) ) & not ( b3 = b5 + 1 & (LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1))) /\ (LSeg (b1 * b4,b5),(b1 * b4,(b5 + 1))) = {(b1 * b2,b3)} ) holds
( b3 + 1 = b5 & (LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1))) /\ (LSeg (b1 * b4,b5),(b1 * b4,(b5 + 1))) = {(b1 * b4,b5)} )
proof end;

theorem Th25: :: GOBOARD7:25
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 + 1 <= len b1 & 1 <= b3 & b3 <= width b1 & 1 <= b4 & b4 + 1 <= len b1 & 1 <= b5 & b5 <= width b1 & LSeg (b1 * b2,b3),(b1 * (b2 + 1),b3) meets LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5) & not ( b2 = b4 & LSeg (b1 * b2,b3),(b1 * (b2 + 1),b3) = LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5) ) & not ( b2 = b4 + 1 & (LSeg (b1 * b2,b3),(b1 * (b2 + 1),b3)) /\ (LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5)) = {(b1 * b2,b3)} ) holds
( b2 + 1 = b4 & (LSeg (b1 * b2,b3),(b1 * (b2 + 1),b3)) /\ (LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5)) = {(b1 * b4,b5)} )
proof end;

theorem Th26: :: GOBOARD7:26
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 + 1 <= width b1 & 1 <= b4 & b4 + 1 <= len b1 & 1 <= b5 & b5 <= width b1 & LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1)) meets LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5) & not ( b3 = b5 & (LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1))) /\ (LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5)) = {(b1 * b2,b3)} ) holds
( b3 + 1 = b5 & (LSeg (b1 * b2,b3),(b1 * b2,(b3 + 1))) /\ (LSeg (b1 * b4,b5),(b1 * (b4 + 1),b5)) = {(b1 * b2,(b3 + 1))} )
proof end;

Lemma21: 1 - (1 / 2) = 1 / 2
;

theorem Th27: :: GOBOARD7:27
for b1, b2, b3, b4 being Nat
for b5 being Go-board st 1 <= b1 & b1 <= len b5 & 1 <= b2 & b2 + 1 <= width b5 & 1 <= b3 & b3 <= len b5 & 1 <= b4 & b4 + 1 <= width b5 & (1 / 2) * ((b5 * b1,b2) + (b5 * b1,(b2 + 1))) in LSeg (b5 * b3,b4),(b5 * b3,(b4 + 1)) holds
( b1 = b3 & b2 = b4 )
proof end;

theorem Th28: :: GOBOARD7:28
for b1, b2, b3, b4 being Nat
for b5 being Go-board st 1 <= b1 & b1 + 1 <= len b5 & 1 <= b2 & b2 <= width b5 & 1 <= b3 & b3 + 1 <= len b5 & 1 <= b4 & b4 <= width b5 & (1 / 2) * ((b5 * b1,b2) + (b5 * (b1 + 1),b2)) in LSeg (b5 * b3,b4),(b5 * (b3 + 1),b4) holds
( b1 = b3 & b2 = b4 )
proof end;

theorem Th29: :: GOBOARD7:29
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 <= width b3 holds
for b4, b5 being Nat holds
( not 1 <= b4 or not b4 <= len b3 or not 1 <= b5 or not b5 + 1 <= width b3 or not (1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),b2)) in LSeg (b3 * b4,b5),(b3 * b4,(b5 + 1)) )
proof end;

theorem Th30: :: GOBOARD7:30
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
for b4, b5 being Nat holds
( not 1 <= b4 or not b4 + 1 <= len b3 or not 1 <= b5 or not b5 <= width b3 or not (1 / 2) * ((b3 * b1,b2) + (b3 * b1,(b2 + 1))) in LSeg (b3 * b4,b5),(b3 * (b4 + 1),b5) )
proof end;

Lemma26: for b1 being standard non constant special_circular_sequence holds len b1 > 1
proof end;

theorem Th31: :: GOBOARD7:31
for b1 being Nat
for b2 being non empty standard FinSequence of (TOP-REAL 2) st b1 in dom b2 & b1 + 1 in dom b2 holds
b2 /. b1 <> b2 /. (b1 + 1)
proof end;

theorem Th32: :: GOBOARD7:32
for b1 being standard non constant special_circular_sequence ex b2 being Nat st
( b2 in dom b1 & (b1 /. b2) `1 <> (b1 /. 1) `1 )
proof end;

theorem Th33: :: GOBOARD7:33
for b1 being standard non constant special_circular_sequence ex b2 being Nat st
( b2 in dom b1 & (b1 /. b2) `2 <> (b1 /. 1) `2 )
proof end;

theorem Th34: :: GOBOARD7:34
for b1 being standard non constant special_circular_sequence holds len (GoB b1) > 1
proof end;

theorem Th35: :: GOBOARD7:35
for b1 being standard non constant special_circular_sequence holds width (GoB b1) > 1
proof end;

theorem Th36: :: GOBOARD7:36
for b1 being standard non constant special_circular_sequence holds len b1 > 4
proof end;

theorem Th37: :: GOBOARD7:37
for b1 being circular s.c.c. FinSequence of (TOP-REAL 2) st len b1 > 4 holds
for b2, b3 being Nat st 1 <= b2 & b2 < b3 & b3 < len b1 holds
b1 /. b2 <> b1 /. b3
proof end;

theorem Th38: :: GOBOARD7:38
for b1 being standard non constant special_circular_sequence
for b2, b3 being Nat st 1 <= b2 & b2 < b3 & b3 < len b1 holds
b1 /. b2 <> b1 /. b3
proof end;

theorem Th39: :: GOBOARD7:39
for b1 being standard non constant special_circular_sequence
for b2, b3 being Nat st 1 < b2 & b2 < b3 & b3 <= len b1 holds
b1 /. b2 <> b1 /. b3
proof end;

theorem Th40: :: GOBOARD7:40
for b1 being standard non constant special_circular_sequence
for b2 being Nat st 1 < b2 & b2 <= len b1 & b1 /. b2 = b1 /. 1 holds
b2 = len b1
proof end;

theorem Th41: :: GOBOARD7:41
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 <= len (GoB b3) & 1 <= b2 & b2 + 1 <= width (GoB b3) & (1 / 2) * (((GoB b3) * b1,b2) + ((GoB b3) * b1,(b2 + 1))) in L~ b3 holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 <= len b3 & LSeg ((GoB b3) * b1,b2),((GoB b3) * b1,(b2 + 1)) = LSeg b3,b4 )
proof end;

theorem Th42: :: GOBOARD7:42
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b3) & 1 <= b2 & b2 <= width (GoB b3) & (1 / 2) * (((GoB b3) * b1,b2) + ((GoB b3) * (b1 + 1),b2)) in L~ b3 holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 <= len b3 & LSeg ((GoB b3) * b1,b2),((GoB b3) * (b1 + 1),b2) = LSeg b3,b4 )
proof end;

theorem Th43: :: GOBOARD7:43
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * (b1 + 1),b2 )
proof end;

theorem Th44: :: GOBOARD7:44
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 <= len (GoB b4) & 1 <= b2 & b2 + 1 < width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * b1,(b2 + 2)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,b2),((GoB b4) * b1,(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,(b2 + 2) & b4 /. (b3 + 1) = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * b1,b2 )
proof end;

theorem Th45: :: GOBOARD7:45
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,b2),((GoB b4) * b1,(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 1) = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * b1,b2 )
proof end;

theorem Th46: :: GOBOARD7:46
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * b1,(b2 + 1) )
proof end;

theorem Th47: :: GOBOARD7:47
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 < len (GoB b4) & 1 <= b2 & b2 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 2),b2) = LSeg b4,b3 & LSeg ((GoB b4) * b1,b2),((GoB b4) * (b1 + 1),b2) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * (b1 + 2),b2 & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 2) = (GoB b4) * b1,b2 )
proof end;

theorem Th48: :: GOBOARD7:48
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,b2),((GoB b4) * (b1 + 1),b2) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 2) = (GoB b4) * b1,b2 )
proof end;

theorem Th49: :: GOBOARD7:49
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * b1,(b2 + 1) )
proof end;

theorem Th50: :: GOBOARD7:50
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 <= len (GoB b4) & 1 <= b2 & b2 + 1 < width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,b2),((GoB b4) * b1,(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * b1,(b2 + 2)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,b2 & b4 /. (b3 + 1) = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * b1,(b2 + 2) )
proof end;

theorem Th51: :: GOBOARD7:51
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,b2),((GoB b4) * b1,(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,b2 & b4 /. (b3 + 1) = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * (b1 + 1),(b2 + 1) )
proof end;

theorem Th52: :: GOBOARD7:52
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,(b2 + 1)),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,b3 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,(b2 + 1) & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),(b2 + 1) & b4 /. (b3 + 2) = (GoB b4) * (b1 + 1),b2 )
proof end;

theorem Th53: :: GOBOARD7:53
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 < len (GoB b4) & 1 <= b2 & b2 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,b2),((GoB b4) * (b1 + 1),b2) = LSeg b4,b3 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 2),b2) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,b2 & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 2) = (GoB b4) * (b1 + 2),b2 )
proof end;

theorem Th54: :: GOBOARD7:54
for b1, b2, b3 being Nat
for b4 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b4) & 1 <= b2 & b2 + 1 <= width (GoB b4) & 1 <= b3 & b3 + 1 < len b4 & LSeg ((GoB b4) * b1,b2),((GoB b4) * (b1 + 1),b2) = LSeg b4,b3 & LSeg ((GoB b4) * (b1 + 1),b2),((GoB b4) * (b1 + 1),(b2 + 1)) = LSeg b4,(b3 + 1) holds
( b4 /. b3 = (GoB b4) * b1,b2 & b4 /. (b3 + 1) = (GoB b4) * (b1 + 1),b2 & b4 /. (b3 + 2) = (GoB b4) * (b1 + 1),(b2 + 1) )
proof end;

theorem Th55: :: GOBOARD7:55
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 <= len (GoB b3) & 1 <= b2 & b2 + 1 < width (GoB b3) & LSeg ((GoB b3) * b1,b2),((GoB b3) * b1,(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * b1,(b2 + 2)) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * b1,(b2 + 1) & ( ( b3 /. 2 = (GoB b3) * b1,b2 & b3 /. ((len b3) -' 1) = (GoB b3) * b1,(b2 + 2) ) or ( b3 /. 2 = (GoB b3) * b1,(b2 + 2) & b3 /. ((len b3) -' 1) = (GoB b3) * b1,b2 ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * b1,(b2 + 1) & ( ( b3 /. b4 = (GoB b3) * b1,b2 & b3 /. (b4 + 2) = (GoB b3) * b1,(b2 + 2) ) or ( b3 /. b4 = (GoB b3) * b1,(b2 + 2) & b3 /. (b4 + 2) = (GoB b3) * b1,b2 ) ) )
proof end;

theorem Th56: :: GOBOARD7:56
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b3) & 1 <= b2 & b2 + 1 <= width (GoB b3) & LSeg ((GoB b3) * b1,b2),((GoB b3) * b1,(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * b1,(b2 + 1) & ( ( b3 /. 2 = (GoB b3) * b1,b2 & b3 /. ((len b3) -' 1) = (GoB b3) * (b1 + 1),(b2 + 1) ) or ( b3 /. 2 = (GoB b3) * (b1 + 1),(b2 + 1) & b3 /. ((len b3) -' 1) = (GoB b3) * b1,b2 ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * b1,(b2 + 1) & ( ( b3 /. b4 = (GoB b3) * b1,b2 & b3 /. (b4 + 2) = (GoB b3) * (b1 + 1),(b2 + 1) ) or ( b3 /. b4 = (GoB b3) * (b1 + 1),(b2 + 1) & b3 /. (b4 + 2) = (GoB b3) * b1,b2 ) ) )
proof end;

theorem Th57: :: GOBOARD7:57
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b3) & 1 <= b2 & b2 + 1 <= width (GoB b3) & LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * (b1 + 1),(b2 + 1)),((GoB b3) * (b1 + 1),b2) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * (b1 + 1),(b2 + 1) & ( ( b3 /. 2 = (GoB b3) * b1,(b2 + 1) & b3 /. ((len b3) -' 1) = (GoB b3) * (b1 + 1),b2 ) or ( b3 /. 2 = (GoB b3) * (b1 + 1),b2 & b3 /. ((len b3) -' 1) = (GoB b3) * b1,(b2 + 1) ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * (b1 + 1),(b2 + 1) & ( ( b3 /. b4 = (GoB b3) * b1,(b2 + 1) & b3 /. (b4 + 2) = (GoB b3) * (b1 + 1),b2 ) or ( b3 /. b4 = (GoB b3) * (b1 + 1),b2 & b3 /. (b4 + 2) = (GoB b3) * b1,(b2 + 1) ) ) )
proof end;

theorem Th58: :: GOBOARD7:58
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 < len (GoB b3) & 1 <= b2 & b2 <= width (GoB b3) & LSeg ((GoB b3) * b1,b2),((GoB b3) * (b1 + 1),b2) c= L~ b3 & LSeg ((GoB b3) * (b1 + 1),b2),((GoB b3) * (b1 + 2),b2) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * (b1 + 1),b2 & ( ( b3 /. 2 = (GoB b3) * b1,b2 & b3 /. ((len b3) -' 1) = (GoB b3) * (b1 + 2),b2 ) or ( b3 /. 2 = (GoB b3) * (b1 + 2),b2 & b3 /. ((len b3) -' 1) = (GoB b3) * b1,b2 ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * (b1 + 1),b2 & ( ( b3 /. b4 = (GoB b3) * b1,b2 & b3 /. (b4 + 2) = (GoB b3) * (b1 + 2),b2 ) or ( b3 /. b4 = (GoB b3) * (b1 + 2),b2 & b3 /. (b4 + 2) = (GoB b3) * b1,b2 ) ) )
proof end;

theorem Th59: :: GOBOARD7:59
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b3) & 1 <= b2 & b2 + 1 <= width (GoB b3) & LSeg ((GoB b3) * b1,b2),((GoB b3) * (b1 + 1),b2) c= L~ b3 & LSeg ((GoB b3) * (b1 + 1),b2),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * (b1 + 1),b2 & ( ( b3 /. 2 = (GoB b3) * b1,b2 & b3 /. ((len b3) -' 1) = (GoB b3) * (b1 + 1),(b2 + 1) ) or ( b3 /. 2 = (GoB b3) * (b1 + 1),(b2 + 1) & b3 /. ((len b3) -' 1) = (GoB b3) * b1,b2 ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * (b1 + 1),b2 & ( ( b3 /. b4 = (GoB b3) * b1,b2 & b3 /. (b4 + 2) = (GoB b3) * (b1 + 1),(b2 + 1) ) or ( b3 /. b4 = (GoB b3) * (b1 + 1),(b2 + 1) & b3 /. (b4 + 2) = (GoB b3) * b1,b2 ) ) )
proof end;

theorem Th60: :: GOBOARD7:60
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 + 1 <= len (GoB b3) & 1 <= b2 & b2 + 1 <= width (GoB b3) & LSeg ((GoB b3) * (b1 + 1),b2),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * (b1 + 1),(b2 + 1)),((GoB b3) * b1,(b2 + 1)) c= L~ b3 & not ( b3 /. 1 = (GoB b3) * (b1 + 1),(b2 + 1) & ( ( b3 /. 2 = (GoB b3) * (b1 + 1),b2 & b3 /. ((len b3) -' 1) = (GoB b3) * b1,(b2 + 1) ) or ( b3 /. 2 = (GoB b3) * b1,(b2 + 1) & b3 /. ((len b3) -' 1) = (GoB b3) * (b1 + 1),b2 ) ) ) holds
ex b4 being Nat st
( 1 <= b4 & b4 + 1 < len b3 & b3 /. (b4 + 1) = (GoB b3) * (b1 + 1),(b2 + 1) & ( ( b3 /. b4 = (GoB b3) * (b1 + 1),b2 & b3 /. (b4 + 2) = (GoB b3) * b1,(b2 + 1) ) or ( b3 /. b4 = (GoB b3) * b1,(b2 + 1) & b3 /. (b4 + 2) = (GoB b3) * (b1 + 1),b2 ) ) )
proof end;

theorem Th61: :: GOBOARD7:61
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 < len (GoB b3) & 1 <= b2 & b2 + 1 < width (GoB b3) & LSeg ((GoB b3) * b1,b2),((GoB b3) * b1,(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * b1,(b2 + 2)) c= L~ b3 holds
not LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3
proof end;

theorem Th62: :: GOBOARD7:62
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 < len (GoB b3) & 1 <= b2 & b2 + 1 < width (GoB b3) & LSeg ((GoB b3) * (b1 + 1),b2),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3 & LSeg ((GoB b3) * (b1 + 1),(b2 + 1)),((GoB b3) * (b1 + 1),(b2 + 2)) c= L~ b3 holds
not LSeg ((GoB b3) * b1,(b2 + 1)),((GoB b3) * (b1 + 1),(b2 + 1)) c= L~ b3
proof end;

theorem Th63: :: GOBOARD7:63
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 < width (GoB b3) & 1 <= b2 & b2 + 1 < len (GoB b3) & LSeg ((GoB b3) * b2,b1),((GoB b3) * (b2 + 1),b1) c= L~ b3 & LSeg ((GoB b3) * (b2 + 1),b1),((GoB b3) * (b2 + 2),b1) c= L~ b3 holds
not LSeg ((GoB b3) * (b2 + 1),b1),((GoB b3) * (b2 + 1),(b1 + 1)) c= L~ b3
proof end;

theorem Th64: :: GOBOARD7:64
for b1, b2 being Nat
for b3 being standard non constant special_circular_sequence st 1 <= b1 & b1 < width (GoB b3) & 1 <= b2 & b2 + 1 < len (GoB b3) & LSeg ((GoB b3) * b2,(b1 + 1)),((GoB b3) * (b2 + 1),(b1 + 1)) c= L~ b3 & LSeg ((GoB b3) * (b2 + 1),(b1 + 1)),((GoB b3) * (b2 + 2),(b1 + 1)) c= L~ b3 holds
not LSeg ((GoB b3) * (b2 + 1),b1),((GoB b3) * (b2 + 1),(b1 + 1)) c= L~ b3
proof end;