:: On the Go Board of a Standard Special Circular Sequence
:: by Andrzej Trybulec
::
:: Received October 15, 1995
:: Copyright (c) 1995-2021 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 (TOP-REAL n) st p + p1 = q + p1 holds
p = q

proof end;

theorem :: GOBOARD7:4

for n being Nat
for p, p1, q being Point of (TOP-REAL n) st p1 + p = p1 + q holds
p = q by Th3;

theorem Th5: :: GOBOARD7:5

for p, q, p1 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 V8() 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 (TOP-REAL 2) 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 V8() 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 V8() 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 V8() standard special_circular_sequence holds len (GoB f) > 1

proof end;

theorem :: GOBOARD7:33

for f being V8() standard special_circular_sequence holds width (GoB f) > 1

proof end;

theorem Th34: :: GOBOARD7:34

for f being V8() standard special_circular_sequence holds len f > 4

proof end;

theorem Th35: :: GOBOARD7:35

for f being circular s.c.c. FinSequence of (TOP-REAL 2) 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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;