Reverse-order safety for $\varepsilon$-orders

Let $P=(p_1,\dots,p_n)$ be a finite list of integers listed in strictly decreasing $\prec_\varepsilon$-order ($p_j\prec_\varepsilon p_i$ whenever $i<j$). Then $P$ is safe for $\prec_\varepsilon$: the completion order (first $P$ in list order, then the remaining integers in $\prec_\varepsilon$-order) contains no monotone $4$-term progression.

This is the $\mathbb{Z}$-version of Ho's Lemma 1, the base case of the extension procedure.

Formalization Note compLt R P x y holds when both lie in P with x at a smaller index, or x ∈ P and y ∉ P, or neither lies in P and R x y. Safe R P says there are no a and r ≠ 0 with compLt R P a (a+r), compLt R P (a+r) (a+2r) and compLt R P (a+2r) (a+3r). epsLt ε x y is x ≠ y ∧ (x / 2^k % 2 = 1 ↔ ε k = true) with k = padicValInt 2 (y - x), i.e. $k=\nu_2(y-x)$; integer division is floor division, so x / 2^k % 2 is the $k$-th two's-complement digit of $x$.