:: On the Go Board of a Standard Special Circular Sequence :: by Andrzej Trybulec :: :: Received October 15, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin theorem Th1: :: GOBOARD7:1 for r1, r2, s being Real holds ( not abs (r1 - r2) > s or r1 + s < r2 or r2 + s < r1 ) proofend; theorem Th2: :: GOBOARD7:2 for r, s being Real holds ( abs (r - s) = 0 iff r = s ) proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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) proofend; theorem :: GOBOARD7:9 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))) proofend; theorem Th10: :: GOBOARD7:10 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 ) ) proofend; theorem Th11: :: GOBOARD7:11 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 ) ) proofend; theorem :: GOBOARD7:12 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 proofend; begin theorem Th13: :: GOBOARD7:13 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)))} proofend; theorem Th14: :: GOBOARD7:14 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))} proofend; theorem Th15: :: GOBOARD7:15 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)))} proofend; theorem Th16: :: GOBOARD7:16 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)))} proofend; 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 + 1),j)))) /\ (LSeg ((G * (i,j)),(G * (i,(j + 1))))) = {(G * (i,j))} proofend; 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)),(G * ((i + 1),j)))) /\ (LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) = {(G * ((i + 1),j))} proofend; theorem Th19: :: GOBOARD7:19 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 ) proofend; theorem Th20: :: GOBOARD7:20 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 ) proofend; 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 + 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 ) ) proofend; theorem :: GOBOARD7:22 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))} ) proofend; theorem :: GOBOARD7:23 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))} ) proofend; 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 + 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)))} ) proofend; Lm1: 1 - (1 / 2) = 1 / 2 ; theorem Th25: :: GOBOARD7:25 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 ) proofend; theorem Th26: :: GOBOARD7:26 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 ) proofend; theorem Th27: :: GOBOARD7:27 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)))) ) proofend; theorem Th28: :: GOBOARD7:28 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))) ) proofend; begin Lm2: for f being non constant standard special_circular_sequence holds len f > 1 proofend; theorem Th29: :: GOBOARD7:29 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) proofend; theorem Th30: :: GOBOARD7:30 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 ) proofend; theorem Th31: :: GOBOARD7:31 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 ) proofend; theorem :: GOBOARD7:32 for f being non constant standard special_circular_sequence holds len (GoB f) > 1 proofend; theorem :: GOBOARD7:33 for f being non constant standard special_circular_sequence holds width (GoB f) > 1 proofend; theorem Th34: :: GOBOARD7:34 for f being non constant standard special_circular_sequence holds len f > 4 proofend; 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 Element of NAT st 1 <= i & i < j & j < len f holds f /. i <> f /. j proofend; theorem Th36: :: GOBOARD7:36 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 proofend; theorem Th37: :: GOBOARD7:37 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 proofend; theorem Th38: :: GOBOARD7:38 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 proofend; theorem Th39: :: GOBOARD7:39 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) ) proofend; theorem Th40: :: GOBOARD7:40 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) ) proofend; theorem :: GOBOARD7:41 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) ) proofend; theorem :: GOBOARD7:42 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) ) proofend; 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,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) ) proofend; theorem :: GOBOARD7:44 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)) ) proofend; 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 <= 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) ) proofend; 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)),((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) ) proofend; 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 + 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)) ) proofend; theorem :: GOBOARD7:48 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)) ) proofend; 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,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)) ) proofend; theorem :: GOBOARD7:50 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) ) proofend; 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 <= 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) ) proofend; 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)),((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)) ) proofend; theorem Th53: :: GOBOARD7:53 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) ) ) ) proofend; theorem Th54: :: GOBOARD7:54 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) ) ) ) proofend; theorem Th55: :: GOBOARD7:55 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)) ) ) ) proofend; 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 <= 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) ) ) ) proofend; 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)),((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) ) ) ) proofend; 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 + 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) ) ) ) proofend; theorem :: GOBOARD7:59 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 proofend; theorem :: GOBOARD7:60 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 proofend; theorem :: GOBOARD7:61 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 proofend; theorem :: GOBOARD7:62 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 proofend; :: 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) proofend; 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) proofend;