:: On the Go Board of a Standard Special Circular Sequence
:: by Andrzej Trybulec
::
:: Copyright (c) 1995-2017 Association of Mizar Users

theorem Th1: :: GOBOARD7:1
for s, r1, r2 being Real holds
( not |.(r1 - r2).| > s or r1 + s < r2 or r2 + s < r1 )
proof end;

theorem Th2: :: GOBOARD7:2
for r, s being Real holds
( |.(r - s).| = 0 iff r = s )
proof end;

theorem Th3: :: GOBOARD7:3
for n being Nat
for p, p1, q being Point of () st p + p1 = q + p1 holds
p = q
proof end;

theorem :: GOBOARD7:4
for n being Nat
for p, p1, q being Point of () st p1 + p = p1 + q holds
p = q by Th3;

theorem Th5: :: GOBOARD7:5
for p, q, p1 being Point of () st p1 in LSeg (p,q) & p `1 = q `1 holds
p1 `1 = q `1
proof end;

theorem Th6: :: GOBOARD7:6
for p, q, p1 being Point of () st p1 in LSeg (p,q) & p `2 = q `2 holds
p1 `2 = q `2
proof end;

theorem Th7: :: GOBOARD7:7
for p, q, p1 being Point of () st p `1 = q `1 & q `1 = p1 `1 & p `2 <= q `2 & q `2 <= p1 `2 holds
q in LSeg (p,p1)
proof end;

theorem Th8: :: GOBOARD7:8
for p, q, p1 being Point of () st p `1 <= q `1 & q `1 <= p1 `1 & p `2 = q `2 & q `2 = p1 `2 holds
q in LSeg (p,p1)
proof end;

theorem :: GOBOARD7:9
for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = (1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))
proof end;

theorem Th10: :: GOBOARD7:10
for f being non empty FinSequence of ()
for k being Nat st LSeg (f,k) is horizontal holds
ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )
proof end;

theorem Th11: :: GOBOARD7:11
for f being non empty FinSequence of ()
for k being Nat st LSeg (f,k) is vertical holds
ex i being Nat st
( 1 <= i & i <= len (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `1 = ((GoB f) * (i,1)) `1 ) )
proof end;

theorem :: GOBOARD7:12
for f being non empty FinSequence of ()
for i, j being Nat st f is special & i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) misses L~ f
proof end;

theorem Th13: :: GOBOARD7:13
for i, j being Nat
for G being Go-board st 1 <= i & i <= len G & 1 <= j & j + 2 <= width G holds
(LSeg ((G * (i,j)),(G * (i,(j + 1))))) /\ (LSeg ((G * (i,(j + 1))),(G * (i,(j + 2))))) = {(G * (i,(j + 1)))}
proof end;

theorem Th14: :: GOBOARD7:14
for i, j being Nat
for G being Go-board st 1 <= i & i + 2 <= len G & 1 <= j & j <= width G holds
(LSeg ((G * (i,j)),(G * ((i + 1),j)))) /\ (LSeg ((G * ((i + 1),j)),(G * ((i + 2),j)))) = {(G * ((i + 1),j))}
proof end;

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

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

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

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

theorem Th19: :: GOBOARD7:19
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) holds
( i1 = i2 & |.(j1 - j2).| <= 1 )
proof end;

theorem Th20: :: GOBOARD7:20
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) holds
( j1 = j2 & |.(i1 - i2).| <= 1 )
proof end;

theorem Th21: :: GOBOARD7:21
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) holds
( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )
proof end;

theorem :: GOBOARD7:22
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) & not ( j1 = j2 & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) = LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) ) & not ( j1 = j2 + 1 & (LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i1,j1))} ) holds
( j1 + 1 = j2 & (LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i2,j2))} )
proof end;

theorem :: GOBOARD7:23
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) & not ( i1 = i2 & LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) = LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) & not ( i1 = i2 + 1 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
( i1 + 1 = i2 & (LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} )
proof end;

theorem :: GOBOARD7:24
for G being Go-board
for i1, j1, i2, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) & not ( j1 = j2 & (LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
( j1 + 1 = j2 & (LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,(j1 + 1)))} )
proof end;

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

theorem Th25: :: GOBOARD7:25
for i1, i2, j1, j2 being Nat
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) holds
( i1 = i2 & j1 = j2 )
proof end;

theorem Th26: :: GOBOARD7:26
for i1, i2, j1, j2 being Nat
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & (1 / 2) * ((G * (i1,j1)) + (G * ((i1 + 1),j1))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) holds
( i1 = i2 & j1 = j2 )
proof end;

theorem Th27: :: GOBOARD7:27
for i1, j1 being Nat
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * ((i1 + 1),j1))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) )
proof end;

theorem Th28: :: GOBOARD7:28
for i1, j1 being Nat
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )
proof end;

Lm2: for f being non constant standard special_circular_sequence holds len f > 1
proof end;

theorem Th29: :: GOBOARD7:29
for i being Nat
for f being non empty standard FinSequence of () st i in dom f & i + 1 in dom f holds
f /. i <> f /. (i + 1)
proof end;

theorem Th30: :: GOBOARD7:30
for f being non constant standard special_circular_sequence ex i being Nat st
( i in dom f & (f /. i) `1 <> (f /. 1) `1 )
proof end;

theorem Th31: :: GOBOARD7:31
for f being non constant standard special_circular_sequence ex i being Nat st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )
proof end;

theorem :: GOBOARD7:32
for f being non constant standard special_circular_sequence holds len (GoB f) > 1
proof end;

theorem :: GOBOARD7:33
for f being non constant standard special_circular_sequence holds width (GoB f) > 1
proof end;

theorem Th34: :: GOBOARD7:34
for f being non constant standard special_circular_sequence holds len f > 4
proof end;

theorem Th35: :: GOBOARD7:35
for f being circular s.c.c. FinSequence of () st len f > 4 holds
for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
proof end;

theorem Th36: :: GOBOARD7:36
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
proof end;

theorem Th37: :: GOBOARD7:37
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 < i & i < j & j <= len f holds
f /. i <> f /. j
proof end;

theorem Th38: :: GOBOARD7:38
for f being non constant standard special_circular_sequence
for i being Nat st 1 < i & i <= len f & f /. i = f /. 1 holds
i = len f
proof end;

theorem Th39: :: GOBOARD7:39
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in L~ f holds
ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) )
proof end;

theorem Th40: :: GOBOARD7:40
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f holds
ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )
proof end;

theorem :: GOBOARD7:41
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
proof end;

theorem :: GOBOARD7:42
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) = LSeg (f,k) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) )
proof end;

theorem :: GOBOARD7:43
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) )
proof end;

theorem :: GOBOARD7:44
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) )
proof end;

theorem :: GOBOARD7:45
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 2),j))) = LSeg (f,k) & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * ((i + 2),j) & f /. (k + 1) = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,j) )
proof end;

theorem :: GOBOARD7:46
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,j) )
proof end;

theorem :: GOBOARD7:47
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) )
proof end;

theorem :: GOBOARD7:48
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,j) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * (i,(j + 2)) )
proof end;

theorem :: GOBOARD7:49
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,j) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) )
proof end;

theorem :: GOBOARD7:50
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
proof end;

theorem :: GOBOARD7:51
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 2),j))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,j) & f /. (k + 1) = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 2),j) )
proof end;

theorem :: GOBOARD7:52
for i, j, k being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,j) & f /. (k + 1) = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) )
proof end;

theorem Th53: :: GOBOARD7:53
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len 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 = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )
proof end;

theorem Th54: :: GOBOARD7:54
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )
proof end;

theorem Th55: :: GOBOARD7:55
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * ((i + 1),j))) c= L~ f & not ( f /. 1 = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. 2 = (GoB f) * (i,(j + 1)) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),j) ) or ( f /. 2 = (GoB f) * ((i + 1),j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 1)) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len 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 = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) ) )
proof end;

theorem Th56: :: GOBOARD7:56
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) c= L~ f & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 2),j))) c= L~ f & not ( f /. 1 = (GoB f) * ((i + 1),j) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 2),j) ) or ( f /. 2 = (GoB f) * ((i + 2),j) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len 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 = (GoB f) * ((i + 2),j) & f /. (k + 2) = (GoB f) * (i,j) ) ) )
proof end;

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

theorem Th58: :: GOBOARD7:58
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * (i,(j + 1)))) c= L~ f & not ( f /. 1 = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. 2 = (GoB f) * ((i + 1),j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 1)) ) or ( f /. 2 = (GoB f) * (i,(j + 1)) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),j) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len 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 = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) ) )
proof end;

theorem :: GOBOARD7:59
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f holds
not LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f
proof end;

theorem :: GOBOARD7:60
for i, j being Nat
for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * ((i + 1),(j + 2)))) c= L~ f holds
not LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f
proof end;

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

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

:: Moved from JORDAN15, AK, 22.02.2006
theorem :: GOBOARD7:63
for p, q, p1, q1 being Point of () st LSeg (p,q) is vertical & LSeg (p1,q1) is vertical & p `1 = p1 `1 & p `2 <= p1 `2 & p1 `2 <= q1 `2 & q1 `2 <= q `2 holds
LSeg (p1,q1) c= LSeg (p,q)
proof end;

theorem :: GOBOARD7:64
for p, q, p1, q1 being Point of () st LSeg (p,q) is horizontal & LSeg (p1,q1) is horizontal & p `2 = p1 `2 & p `1 <= p1 `1 & p1 `1 <= q1 `1 & q1 `1 <= q `1 holds
LSeg (p1,q1) c= LSeg (p,q)
proof end;