:: On the Go Board of a Standard Special Circular Sequence
:: by Andrzej Trybulec
::
:: Received October 15, 1995
:: Copyright (c) 1995 Association of Mizar Users

theorem Th1: :: GOBOARD7:1

for r1, r2, s being Real holds
( not abs (r1 - r2) > s or r1 + s < r2 or r2 + s < r1 )

proof end;

theorem Th2: :: GOBOARD7:2

for r, s being Real holds
( abs (r - s) = 0 iff r = s )

proof end;

theorem Th3: :: GOBOARD7:3

for n being Element of 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 Element of 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 p1, p, q 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 p1, p, q 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 n being Element of NAT
for p, q being Point of (TOP-REAL n) holds (1 / 2) * (p + q) in LSeg p,q

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 Th9: :: GOBOARD7:9

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:10

canceled;

theorem :: GOBOARD7:11

for i, j being Element of 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 Th12: :: GOBOARD7:12

for f being non empty FinSequence of (TOP-REAL 2)
for k being Element of NAT st LSeg f,k is horizontal holds
ex j being Element of 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 Th13: :: GOBOARD7:13

for f being non empty FinSequence of (TOP-REAL 2)
for k being Element of NAT st LSeg f,k is vertical holds
ex i being Element of 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:14

for f being non empty FinSequence of (TOP-REAL 2)
for i, j being Element of 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 Th15: :: GOBOARD7:15

for i, j being Element of 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 Th16: :: GOBOARD7:16

for i, j being Element of 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 Th17: :: GOBOARD7:17

for i, j being Element of 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 Th18: :: GOBOARD7:18

for i, j being Element of 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 Th19: :: GOBOARD7:19

for i, j being Element of 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 Th20: :: GOBOARD7:20

for i, j being Element of 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 Th21: :: GOBOARD7:21

for G being Go-board
for i1, j1, i2, j2 being Element of 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 & abs (j1 - j2) <= 1 )

proof end;

theorem Th22: :: GOBOARD7:22

for G being Go-board
for i1, j1, i2, j2 being Element of 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 & abs (i1 - i2) <= 1 )

proof end;

theorem Th23: :: GOBOARD7:23

for G being Go-board
for i1, j1, i2, j2 being Element of 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:24

for G being Go-board
for i1, j1, i2, j2 being Element of 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:25

for G being Go-board
for i1, j1, i2, j2 being Element of 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:26

for G being Go-board
for i1, j1, i2, j2 being Element of 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 Th27: :: GOBOARD7:27

for i1, j1, i2, j2 being Element of 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 Th28: :: GOBOARD7:28

for i1, j1, i2, j2 being Element of 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 Th29: :: GOBOARD7:29

for i1, j1 being Element of NAT
for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G holds
for i2, j2 being Element of 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 Th30: :: GOBOARD7:30

for i1, j1 being Element of NAT
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G holds
for i2, j2 being Element of 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 Th31: :: GOBOARD7:31

for i being Element of 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 Th32: :: GOBOARD7:32

for f being non constant standard special_circular_sequence ex i being Element of NAT st
( i in dom f & (f /. i) `1 <> (f /. 1) `1 )

proof end;

theorem Th33: :: GOBOARD7:33

for f being non constant standard special_circular_sequence ex i being Element of NAT st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )

proof end;

theorem :: GOBOARD7:34

for f being non constant standard special_circular_sequence holds len (GoB f) > 1

proof end;

theorem :: GOBOARD7:35

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

proof end;

theorem Th36: :: GOBOARD7:36

for f being non constant standard special_circular_sequence holds len f > 4

proof end;

theorem Th37: :: GOBOARD7:37

for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
for i, j being Element of 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, j being Element of NAT st 1 <= i & i < j & j < len f holds
f /. i <> f /. j

proof end;

theorem Th39: :: GOBOARD7:39

for f being non constant standard special_circular_sequence
for i, j being Element of NAT st 1 < i & i < j & j <= len f holds
f /. i <> f /. j

proof end;

theorem Th40: :: GOBOARD7:40

for f being non constant standard special_circular_sequence
for i being Element of NAT st 1 < i & i <= len f & f /. i = f /. 1 holds
i = len f

proof end;

theorem Th41: :: GOBOARD7:41

for i, j being Element of 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 Element of NAT st
( 1 <= k & k + 1 <= len f & LSeg ((GoB f) * i,j),((GoB f) * i,(j + 1)) = LSeg f,k )

proof end;

theorem Th42: :: GOBOARD7:42

for i, j being Element of 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 Element of 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:43

for i, j, k being Element of 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:44

for i, j, k being Element of 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:45

for i, j, k being Element of 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:46

for i, j, k being Element of 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:47

for i, j, k being Element of 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:48

for i, j, k being Element of 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:49

for i, j, k being Element of 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:50

for i, j, k being Element of 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:51

for i, j, k being Element of 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:52

for i, j, k being Element of 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:53

for i, j, k being Element of 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:54

for i, j, k being Element of 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 Th55: :: GOBOARD7:55

for i, j being Element of 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 Element of 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 Th56: :: GOBOARD7:56

for i, j being Element of 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 Element of 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 Th57: :: GOBOARD7:57

for i, j being Element of 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 Element of 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 Th58: :: GOBOARD7:58

for i, j being Element of 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 Element of 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 Th59: :: GOBOARD7:59

for i, j being Element of 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 Element of 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 Th60: :: GOBOARD7:60

for i, j being Element of 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 Element of 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:61

for i, j being Element of 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:62

for i, j being Element of 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:63

for j, i being Element of 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:64

for j, i being Element of 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;

theorem :: GOBOARD7:65

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:66

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;