theorem
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