| p |
|
|
| p + r |
|
(≥
0) |
| r |
|
(≥
0) |
| -p |
|
(≤
0) |
| p - r |
|
(≥
0) |
| 2∙p -
r |
|
(≥
0) |
| p |
|
(≥
0) |
| r - p |
|
(≤
0) |
| - r |
|
(≤
0) |
| p |
|
(≥
0) |
| p + r |
|
|
|
From
(0) we conclude (i) that the sequence contains a nonnegative
element, (ii) that one of its neighbours is nonnegative, and (iii)
that at least one of the two elements adjacent to a pair of
nonnegative neighbours is nonnegative. More precisely: the
sequence contains in some direction a triple of adjacent elements
of the form (p, p+r, r) with 0 ≤
r ≤
p. To the left we have extended the sequence with another 8
elements. From (0) we further conclude that the whole sequence is
determined by a pair of adjacent values; hence, the repetition of
the pair (p, p+r) at distance 9 proves the
theorem. [The above deserves recording for its lack of case
analyses.] |