:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

theorem :: GOBOARD8:1

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:2

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:3

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:4

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB 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 + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:5

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB 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 + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:6

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB 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 + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:7

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),1) & ( ( f /. k = (GoB f) * ((i + 2),1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),2))))) misses L~ f

proof end;

theorem :: GOBOARD8:8

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),1) & ( ( f /. k = (GoB f) * (i,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) misses L~ f

proof end;

theorem :: GOBOARD8:9

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:10

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * (i,(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) + ((GoB f) * ((i + 2),(width (GoB f)))))),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:11

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f

proof end;

theorem :: GOBOARD8:12

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f

proof end;

theorem :: GOBOARD8:13

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f

proof end;

theorem :: GOBOARD8:14

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB 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 + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f

proof end;

theorem :: GOBOARD8:15

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:16

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j, i being Nat st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB 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 + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:17

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) misses L~ f

proof end;

theorem :: GOBOARD8:18

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,j) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,j) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (2,(j + 2)))))) misses L~ f

proof end;

theorem :: GOBOARD8:19

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f

proof end;

theorem :: GOBOARD8:20

for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 2 <= len f holds
for j being Nat st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f

proof end;

theorem Th21: :: GOBOARD8:21

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ) holds
P misses L~ f

proof end;

theorem Th22: :: GOBOARD8:22

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) holds
P misses L~ f

proof end;

theorem Th23: :: GOBOARD8:23

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ) holds
P misses L~ f

proof end;

theorem Th24: :: GOBOARD8:24

for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) holds
P misses L~ f

proof end;

theorem :: GOBOARD8:25

for f being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:26

for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:27

for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f

proof end;

theorem :: GOBOARD8:28

for f being non constant standard special_circular_sequence
for i being Nat st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:29

for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:30

for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:31

for f being non constant standard special_circular_sequence
for j being Nat st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f

proof end;

theorem :: GOBOARD8:32

for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f

proof end;

theorem :: GOBOARD8:33

for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:34

for f being non constant standard special_circular_sequence
for j being Nat st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f

proof end;

theorem :: GOBOARD8:35

for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f

proof end;

theorem :: GOBOARD8:36

for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[1,0]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) misses L~ f

proof end;

theorem :: GOBOARD8:37

for k being Nat
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f

proof end;

theorem :: GOBOARD8:38

for k being Nat
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) misses L~ f

proof end;