Proof. We show for Rule 6 first. Suppose that

\[ (c_j,c_{j-1},\dotsc,c_{\ell}) \]

violates Rule 6. Since a non-top rule applies, the subword can only violate either Rule 2 or Rule 6 on a strict smaller subword. If it violates Rule 2, then we pick the coefficient as the poison subword. If it violates Rule 6 on a smaller subword, we pick this subword and repeat the process until we get the minimal poison subword.

For top rules, we only show for Rule 4. Suppose that the subword

\[ (c_m,\dotsc, c_{m-i})=(1,c_{m-1},\dotsc,c_{m-i}) \]

violates Rule 4. If this subword violates some other rules, the violation can only come from Rule 1, Rule 3, Rule 4 and Rule 6. If it violates any of the local rules, then we pick the coefficient in question as the poison subword as before. If it violates Rule 4 on a strictly smaller subword contained in the original, we pick the smaller subword and repeat the same argument again. Hence, it remains to show that if Rule 6 is violated, the violation occurs on a strictly smaller subword. For

\[ (1,c_{m-1},\dotsc,c'_{m-i}), \]

we observe that $c_{m-1}$ is either $-k+1$ or $-k+2$. Since Rule 6 requires the leading coefficient to be $-k$ or $-k-1$, $c_{m-1}$ is not contained in the subword that violates Rule 6. By repeating this process for a strictly smaller subword, we get a poison subword. The case for Rule 5 can be worked out similarly.

Proof. We rule out all of the other possible cases using the potential of subwords. We have a number of cases based on the inclusion relationship between the subwords $(s'_i,\,\dotsc,\,s'_{i-k})$ and $(s'_j,\,\dotsc,\,s'_{j-l})$.

1. (1) The subword $(s'_j,\,\dotsc,\,s'_{j-l})$ is contained in the subword $(s'_i,\,\dotsc,\,s'_{i-k})$. This case is handled by Lemma 18.

2. (2) The subword $(s'_i,\,\dotsc,\,s'_{i-k})$ is contained in the subword $(s'_j,\,\dotsc,\,s'_{j-l})$. This case is handled in Lemma 19. See Figure 3.

3. (3) The subword $(s'_j,\,\dotsc,\,s'_{j-l})$ is on the right of the subword $(s'_i,\,\dotsc,\,s'_{i-k})$. This last case is handled in Lemma 20. See Figure 4.

Proof. We first show that the new poison subword $(s'_j,\,\dotsc,\,s'_{j-l})$ cannot be contained in the subword $(s'_i,\,\dotsc,\,s'_{i-k})$ (see Figure 2.)

Figure 2.

The new minimal poison subword cannot be contained in where the previous minimal poison subword was. (Lemma 18.).

We first list rules we need to check. (See Table 1.) We note that if the initial minimal poison subword violates a local rule, then the next minimal poison subword that appears after rewriting can only violate a local rule because we assumed containment. More specifically, once $(s_{i+1},\,s_i)$ violates Rule 3, we can only check $(s'_i)$ for Rule 1 and vice versa. Similarly, once $(s_i)$ violates Rule 2, we can only check $(s'_i)$ for Rule 2. However, by Definition 8, we know this is impossible. So assume that the initial minimal poison subword violates a global rule as listed in Table 1. We also point out that, because of containment, if the initial rule violation is from a non-top rule, then the next rule violation cannot be from a top rule.

Table 1.

For Lemma 18, we only need to check these rules.

For simplicity, denote the initial minimal poison subword as

\[ (s_i,\dotsc,s_{i-k})=(A|B|C) \]

as 3 disjoint subwords concatenated into one word. After rewriting, this subword becomes $(s'_i,\,\dotsc,\,s'_{i-k})$, which we denote $(A'|B'|C')$ where $(s'_j,\,\dotsc,\,s'_{j-l})=(B')$. The rewriting rule in this case is

\begin{align*} & (s_{i+1}, |A|B|C|,s_{i-k-1})-\operatorname{sign}(s_i)({-}1,2k,2k-1,\dotsc,2k-1,2k,-1)\\ & =(s'_{i+1}, |A'|B'|C'|, s'_{i-k-1}). \end{align*}

For a top rule, subword $(A)$ is empty. Obviously, the subwords $(A)$ and $(C)$ cannot be empty at the same time, as the rules cannot be applied to the same subword twice by Definition 8.

We argue in the following way: because the subword $(A'|B'|C')$ was obtained from rewriting, there's a bound on the value $\operatorname {Pot}(A'|B'|C')$ from which comes from the value $\operatorname {Pot}(A|B|C)$. Since the subword $(B')$ violates one of the rules, we can combine with alternate bounds on the values $\operatorname {Pot}(A')$ and $\operatorname {Pot}(C')$ to get another bound on the value $\operatorname {Pot}(A'|B'|C')$ which contradicts the previous bound on the value of $\operatorname {Pot}(A'|B'|C')$. We proceed through our proof based on the particular rule that the subword $(A|B|C)$ violates. In each case, we assume that either $j \leq i$ or $j-l \leq i -k$ for our contradiction.

1. $(A|B|C)$ violates Rule 4 or Rule 5.

As mentioned, $(A)$ and $(C)$ cannot be both empty. We proceed based on whether $(A)$, $(C)$, or $(A)$ and $(C)$ are both empty.

1. (1) Suppose that both $(A)$ and $(C)$ are nonempty.

   It then follows that the word $(B')$ can only violate Rule 2 or Rule 6. Since all coefficients in $(B')$ have values either $\pm k$ or $\pm (k-1)$, and all coefficients in $(A'|B'|C')$ have the same sign, Rule 2 cannot be violated. As for Rule 6, when $(A|B|C)$ violates Rule 4, we then have

   \begin{align*} \operatorname{Pot}(A|B|C) & \leq 1+ \tfrac{1}{2}\operatorname{sign}^-(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq{-}4,\\ \operatorname{Pot}(C')& ={-}\operatorname{Pot}(C)-2\leq 1+\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(B') & \leq{-}4. \end{align*}
   This implies that
   \[ \operatorname{Pot}(A'|B'|C')\leq{-}7+\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}). \]
   But $\operatorname {Pot}(A'|B'|C') \geq -5- \tfrac {1}{2}\operatorname {sign}^-(s_{i-k} \cdot s_{i-k-1})$ which is impossible.

   Similarly, when $(A|B|C)$ violates Rule 5 and $(B')$ violates Rule 6, we have

   \begin{align*} \operatorname{Pot}(A|B|C) & \leq{-}5- \tfrac{1}{2}\operatorname{sign}^+(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq 3,\\ \operatorname{Pot}(C')& ={-}\operatorname{Pot}(C)-2\leq 1+\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(B') & \leq{-}4. \end{align*}
   Taking this all together, we may write
   \[ \operatorname{Pot}(A'|B'|C')\leq \tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}). \]
   But $\operatorname {Pot}(A'|B'|C') \geq 1+ \tfrac {1}{2}\operatorname {sign}^+(s_{i-k} \cdot s_{i-k-1})$ which is impossible.

2. (2) $(C)$ is empty.

   The above argument works identically. Assuming that $(B)$ is violating Rule 6, the potential is bounded

   \begin{align*} \operatorname{Pot}(A|B) & \leq 1+ \tfrac{1}{2}\operatorname{sign}^-(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq{-}4,\\ \operatorname{Pot}(B') & \leq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(A'|B')& \leq{-}7-\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(A'|B') & \geq{-}5- \tfrac{1}{2}\operatorname{sign}^-(s_{i-k} \cdot s_{i-k-1}) \end{align*}
   for Rule 4, which is impossible. For Rule 5, we have that
   \begin{align*} \operatorname{Pot}(A|B) & \leq{-}5- \tfrac{1}{2}\operatorname{sign}^+(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq 3,\\ \operatorname{Pot}(B') & \leq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(A'|B')& \leq{-}\tfrac{1}{2}\operatorname{sign}^+(s_{i-k}\cdot s_{i-k-1}),\\ \operatorname{Pot}(A'|B')& \geq 1+\tfrac{1}{2}\operatorname{sign}^+(s_{i-k} \cdot s_{i-k-1}). \end{align*}
   which is impossible. For Rule 2, we only need to consider $(B')=s'_{i-k}$. The only possible coefficients for $s'_{i-k}$ are $\pm k$ and $\pm (k-1)$, and $s'_{i-k+1}$ has the same sign as $s'_{i-k}$, so $s'_{i-k}$ cannot violate Rule 2.

3. (3) $(A)$ is empty.

   If $(B|C)$ violates Rule 4 then $(B')$ violates Rule 1 or Rule 5, and if $(B|C)$ violates Rule 5, then $(B')$ violates Rule 3 or Rule 4. Suppose that $(B|C)$ violates Rule 4. Since $(s'_{i})$ is either $\pm (k+1)$ or $\pm (k+1)$ with $(s'_{i-1})$ having the same sign as $(s'_{i})$, Rule 1 cannot be violated. As for Rule 5, we check the potential

   \begin{align*} \operatorname{Pot}(B|C) & \leq 1+ \tfrac{1}{2}\operatorname{sign}^-(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(C')& \geq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}),\\ \operatorname{Pot}(C)& \geq 1+\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}),\\ \operatorname{Pot}(B') & \leq{-}5,\\ \operatorname{Pot}(B) & \geq 3,\\ \operatorname{Pot}(B|C)& \geq 4+\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}). \end{align*}
   which is impossible. Now suppose that $(B|C)$ violates Rule 5. For Rule 3, $(B)=s'_{i}$ is either $\pm (k-1)$ or $\pm (k-2)$, with $s'_{i}$ having the same sign as $s'_{i}$, so Rule 3 cannot be violated. For Rule 4, We have that
   \begin{align*} \operatorname{Pot}(B|C) & \leq{-}5- \tfrac{1}{2}\operatorname{sign}^+(s_{i-k} \cdot s_{i-k-1}),\\ \operatorname{Pot}(C')& \geq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}),\\ \operatorname{Pot}(C)& \geq 1+\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}),\\ \operatorname{Pot}(B') & \leq 1,\\ \operatorname{Pot}(B) & \geq{-}3,\\ \operatorname{Pot}(B|C)& \geq{-}2+\tfrac{1}{2}\operatorname{sign}^+(s'_{i-k}\cdot s'_{i-k-1}) \end{align*}
   which is impossible.

2. The subword $(A|B|C)$ violates Rule 6

First, we can rule out Rule 2 entirely, as the coefficients appearing in $(A')$, $(B')$ and $(C')$ are either $\pm k$ or $\pm (k-1)$, with at least one neighbouring coefficient having the same sign. So suppose that $(B')$ violates Rule 6. We proceed based on whether $A$, $C$ or $A$ and $C$ are empty.

1. (1) The subwords $(A)$ and $(C)$ are both nonempty.

   Recall that the subword $(s_i,\,\dotsc,\,s_{i-k})$ satisfies Rule 6 if

   \[ \operatorname{Pot}(s_i,\dotsc,s_{i-k}) \geq{-}2- \operatorname{sign}^+(s_i \cdot s_{i+1})- \tfrac{1}{2}\operatorname{sign}^+(s_i \cdot s_{i-k-1}). \]
   Since the subword $(s_i,\,\dotsc,\,s_{i-k})=(A|B|C)$ violates Rule 6, we instead have
   \[ \operatorname{Pot}(A|B|C) \leq{-}2- \operatorname{sign}^+(s_i \cdot s_{i+1})-\tfrac{1}{2}\operatorname{sign}^+(s_i \cdot s_{i-k-1}). \]
   Since the subword $(A|B|C)$ is minimal, none of the subwords inside $(A|B|C)$ violate any rules which includes Rule 6. Thus, we have
   \begin{align*} \operatorname{Pot}(A) & \geq{-}2- \operatorname{sign}^+(s_i \cdot s_{i+1})- \tfrac{1}{2}\operatorname{sign}^+(A \cdot B),\\ \operatorname{Pot}(A) & \geq{-}2- \operatorname{sign}^+(s_i \cdot s_{i+1}),\\ \operatorname{Pot}(C) & \geq{-}2- \operatorname{sign}^+(B \cdot C)-\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}),\\ \operatorname{Pot}(C) & \geq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}). \end{align*}
   After rewriting, the subword $(B')$ is the rightmost minimal poison subword violating Rule 6. Therefore, we have
   \[ \operatorname{Pot}(B') \leq{-}2- \operatorname{sign}^+(A'\cdot B')- \operatorname{sign}^+(B'\cdot C')={-}4. \]
   Because $(A'|B'|C')$ was obtained from $(A|B|C)$ by rewriting, we have
   \begin{align*} \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq \operatorname{sign}^+(s_i \cdot s_{i+1}),\\ \operatorname{Pot}(C')& ={-}\operatorname{Pot}(C)-2\leq 1+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}). \end{align*}
   Hence, we may write the value $\operatorname {Pot}(A'|B'|C')$ as
   \[ -\operatorname{Pot}(A|B|C)-4\geq{-}2+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i \cdot s_{i-k-1}). \]
   But $\operatorname {Pot}(B')\leq -4$. Therefore,
   \[ \operatorname{Pot}(A'|B'|C')\leq{-}3+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}) \]
   which is a contradiction.

2. (2) $(A)$ is empty.

   We may write

   \begin{align*} \operatorname{Pot}(B')& \leq{-}3-\operatorname{sign}^+(s'_i \cdot s'_{i+1}),\\ \operatorname{Pot}(C')& \leq 1+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}) \end{align*}
   Therefore, we may express $\operatorname {Pot}(B'|C')$ as
   \[ -\operatorname{Pot}(B|C)-4\geq{-}2+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}). \]
   However, since $\operatorname {sign}^-(s_i \cdot s'_{i+1})\leq \operatorname {sign}^+(s_i \cdot s_{i+1})$, we have that
   \begin{align*} \operatorname{Pot}(B'|C')& \leq{-}2-\operatorname{sign}^+(s'_i \cdot s'_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}),\\ & ={-}2+\operatorname{sign}^-(s_i \cdot s'_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}),\\ & \leq{-}2+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}),\\ & \leq \operatorname{Pot}(B'|C'). \end{align*}
   Thus, the equality can only happen when $\operatorname {sign}^+(s_i\cdot s_{i-k-1})=0$ which is impossible.

3. (3) $(C)$ is empty.

   We then have

   \begin{align*} \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq \operatorname{sign}^+(s_i \cdot s_{i+1}),\\ \operatorname{Pot}(B')& \leq{-}3+\tfrac{1}{2}\operatorname{sign}^+(s'_i\cdot s'_{i-k-1}). \end{align*}
   That implies we may write $\operatorname {Pot}(A'|B')$ as
   \[ -\operatorname{Pot}(A|B)-4\geq{-}2+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1}). \]
   Hence, we may further write
   \begin{align*} \operatorname{Pot}(A'|B')& \leq{-}3+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s'_i\cdot s'_{i-k-1}),\\ & \leq{-}3+\operatorname{sign}^+(s_i \cdot s_{i+1})+\tfrac{1}{2}\operatorname{sign}^+(s_i\cdot s_{i-k-1})<\operatorname{Pot}(A'|B'). \end{align*}

Proof. Again, we begin with listing rules to be checked. (See Table 2.) Because we have already checked the cases when the second violation is from a local rule in Lemma 18, we only need to check global rules for the second violation.

Table 2.

For Lemma 19, we only need to check these rules. by Lemma 18, the second violation from local rules are ruled out.

Suppose $(B)$ violates Rule 1. Then $(A)$ is empty and $(B')=s'_{m-1}$ is either $\pm (k-1)$ or $\pm (k-2)$. Since $(B)$ is assumed to be the rightmost minimal poison, $(C)$ does not violate Rule 6. By Lemma 10, we have

\[ \operatorname{Pot}(C) \geq{-}1- \tfrac{1}{2}\operatorname{sign}^+(s'_{i-k-1} \cdot s'_{j-\ell-1}). \]

Since $(C')$ is obtained by adding $\operatorname {sign}(B)$ to $s_{i-k-1}$,

\[ \operatorname{Pot}(C') \geq 1- \tfrac{1}{2}\operatorname{sign}^+(s'_{i-k-1} \cdot s'_{j-\ell-1}). \]

Since $(B'|C')$ violates Rule 4, we have

\[ \operatorname{Pot}(B'|C') < 1+\tfrac{1}{2}\operatorname{sign}^-(s'_m\cdot s'_{j-\ell-1}). \]

However, $\operatorname {Pot}(s'_{m-1})>0$, so this is impossible. The case when $(A'|B'|C')$ violates the Rule 4 can be worked out similarly by using a lower bound for $\operatorname {Pot}(B')$ which is obtained from an upper bound for $\operatorname {Pot}(B)$.

Now suppose $(B)$ violates Rule 3. Then $(A)$ is empty and $(B')=s'_{m-1}$ is either $\pm k$ or $\pm (k-1)$. Since $(C)$ does not violate Rule 6, just like before, we have

\[ \operatorname{Pot}(C') \geq 1- \tfrac{1}{2}\operatorname{sign}^+(s'_{i-k-1} \cdot s'_{j-\ell-1}). \]

Since $(B'|C')$ violates Rule 5, we have

\[ \operatorname{Pot}(B'|C') <{-}5- \tfrac{1}{2}\operatorname{sign}^+(c_m \cdot c_{j-\ell-1}). \]

However, $\operatorname {Pot}(s'_{m-1})>-2$, so this is impossible. The case when $(A'|B'|C')$ violates the Rule 5 can be worked out similarly, again by using a lower bound for $\operatorname {Pot}(B')$ which is obtained from an upper bound for $\operatorname {Pot}(B)$.

Suppose both $(B)$ and $(A'|B'|C')$ violate Rule 6, or $(B)$ violates Rule 2 and $(A'|B'|C')$ violate Rule 6. Since $(B)$ is the rightmost, we have that

\[ \operatorname{Pot}(C)\geq{-}1-\tfrac{1}{2}\operatorname{sign}^+(C\cdot s'_{j-l}). \]

Therefore,

\[ \operatorname{Pot}(C')\geq 1-\tfrac{1}{2}\operatorname{sign}^+(C'\cdot s_{j-l}). \]

On the other hand, since $(A'|B'|C')$ violates Rule 6, we have that

\[ \operatorname{Pot}(A'|B'|C')\leq{-}2-\operatorname{sign}^+(s_{j+1}\cdot A')-\tfrac{1}{2} \operatorname{sign}^+(C'\cdot s_{j-l}). \]

This gives us a new bound $\operatorname {Pot}(A'|B')\leq -3-\operatorname {sign}^+(s_{j+1}\cdot A')$ which implies that $(A'|B')$ violates Rule 6, contradicting that $(A'|B'|C')$ is minimal poison. Using the same bounds for $\operatorname {Pot}(C')$, we also get a contradiction for $(A'|B'|C')$ violating Rule 4 or Rule 5.

Proof. We begin with listing rules to be checked. (See Table 3.) By Lemma 18 and 19, regardless of the initial rule violation, the next rule violation can only be from Rule 2 or Rule 6.

Table 3.

For Lemma 20, all other cases have been exhausted except for by Lemma 18 and 19.

Table 4.

Base case for types and classes.

Table 5.

Inductive case for types and classes.

Suppose that $(s_i,\, \ldots,\, s_{i-k})$ violates any of the rules. By Lemma 18, the minimal poison subword violating Rule 2 after rewriting must be disjoint from $(s_i,\, \ldots,\, s_{i-k})$, $(s'_{i-k-1})$ is the minimal poison subword in this case. $(s_{i-k-1})$ is not a poison subword, so by Definition 8,

\[ |s_{i-k-1}|\leq k+1, k, \text{ or } k-1 \]

depending on $\operatorname {sign}(s_{i-k}s_{i-k-1})$ and $\operatorname {sign}(s_{i-k-1}s_{i-k-2})$. $(s'_{i-k-1})$ violates Rule 2, so

\[ |s'_{i-k-1}|> k+1, k, \text{ or } k-1 \]

depending on

\[ \operatorname{sign}(s'_{i-k}s'_{i-k-1})={-}\operatorname{sign}(s_{i-k}s_{i-k-1}) \]

and

\[ \operatorname{sign}(s'_{i-k-1}s_{i-k-2})=\operatorname{sign}(s_{i-k-1}s_{i-k-2}). \]

But this is impossible, since $s'_{i-k-1}=s_{i-k-1}+\operatorname {sign}(s_{i-k})$.

Now we have ruled out all local rules. Suppose $i\geq j\geq i-k\geq j-l$. Let the intersection be $(B')$, $(s'_i,\,\dotsc,\,s'_{i-k})=(A'|B')$, and $(s'_j,\,\dotsc,\,s'_{j-l})=(B'|C')$ is the minimal poison subword violating Rule 6. We show $(B')$ is empty and use the fact that $(A|B)$ is the rightmost minimal poison subword to get a contradiction. In this case, the rewriting is given by

\begin{align*} & (s_{i+1}|A|B|s_{i-k-1})-\operatorname{sign}(s_i)({-}1,2k,2k-1,\dotsc,2k-1,2k,-1)\\ & =(s'_{i+1}|A'|B'|s'_{i-k-1}). \end{align*}

Note that $(A)$ and $(B)$ have the same sign and $(B')$ and $(C')$ have the same sign, since $(A|B)$ and $(B'|C')$ violate some rules. Also, $(B)$ and $(B')$ have opposite signs because of the rewriting. Thus, all coefficients in $(A)$ and $(B)$ have the same sign with all coefficients in $(C)$ the opposite sign.

$(A|B)$ violates Rule 6. Thus,

\begin{align*} \operatorname{Pot}(A|B)& \leq{-}2-\operatorname{sign}^+(s_i\cdot s_{i+1}),\\ \operatorname{Pot}(A)& \geq{-}2- \operatorname{sign}^+(s_i\cdot s_{i+1}) \textbf{(Rule 6)},\\ \operatorname{Pot}(B)& \geq{-}2 \textbf{(Rule 6)},\\ \operatorname{Pot}(C)& \geq{-}1-\tfrac{1}{2}\operatorname{sign}^+(s_{i-k-1}\cdot s_{j-l-1}) \textbf{(Rule 6)},\\ \operatorname{Pot}(B'|C')& \leq{-}3-\tfrac{1}{2}\operatorname{sign}^+(s'_{j-l}\cdot s_{j-l-1}) \text{(Violation of}\, {\textbf{Rule 6})},\\ \operatorname{Pot}(A')& ={-}\operatorname{Pot}(A)-2\leq \operatorname{sign}^+(s_i\cdot s_{i+1}) \text{(Rewriting)},\\ \operatorname{Pot}(A'|B')& \geq{-}2+\operatorname{sign}^+(s_i\cdot s_{i+1}) \text{(Rewriting)}. \end{align*}

By combining the inequalities for $\operatorname {Pot}(A')$ and $\operatorname {Pot}(A'|B')$, we get

\[ \operatorname{Pot}(B')\geq{-}2. \]

Hence, combining the inequalities for $\operatorname {Pot}(B')$ and $\operatorname {Pot}(B'|C')$ allows us to write

\[ \operatorname{Pot}(C')\leq{-}1-\tfrac{1}{2}\operatorname{sign}^+(s'_{j-l}\cdot s_{j-l-1}). \]

However, it then follows that $\operatorname {Pot}(C)\leq -3-\tfrac {1}{2}\operatorname {sign}^+(s'_{j-l}\cdot s_{j-l-1})$ which contradicts the previous bound on $\operatorname {Pot}(C)$. Thus, $(B)$ is empty. Similarly, we can show that $(B)$ is empty assuming $(A|B)$ violates either Rule 4 or Rule 5.

Since the subword $(B)$ is empty, two consecutive poison subwords are disjoint, and thus, we can directly compare the potentials. $(C')$ is a minimal poison subword. Therefore, we have that $\operatorname {Pot}(C')\leq -2-\operatorname {sign}^+(c_{j}\cdot c_{j+1})-\tfrac {1}{2}\operatorname {sign}^+(c_{j-l}\cdot c_{j-l-1})$. Because $(A)$ and $(C)$ has opposite sign, the rewriting rule suggests that $\operatorname {Pot}(C)=\operatorname {Pot}(C')-2$, which means that $(C)$ already violates Rule 6 contradicting the fact $(A)$ is the rightmost minimal poison subword.

Proof. If not, by adding or subtracting $X^d(X^2-(2k+1)X+1)$ with some appropriate choice of $d$, one can obtain a new Laurent polynomial. By Lemma 12, this new Laurent polynomial has strictly less $n$-length, contradicting the fact $F(X)$ is an $n$-minimal representative of $g$.

Proof. We induct on $r$ reversely, i.e., we apply the rewriting procedure as in Theorem 17 on $F(X)$ inductively from a higher degree. The base case in our case for the induction is when $r=m$. Consider $c_m X^m$. Only local rules apply here, and by Lemma 22, $c_m X^m$ is $n$-reduced. Thus, $c_m=B_M$ and $m=M$. For the step case, consider

\[ F_r(X)=c_m X^m + \ldots + c_{r} X^{r}. \]

If it is $n$-reduced, we are done and $m=M$. If not, Lemma 22 implies that $F_r(X)$ cannot violate local rules. Thus, we need only consider global rules. As in Theorem 17, we start rewriting from the rightmost minimal poison subword of $(c_m,\,\dotsc,\,c_r)$. We note that since $F_{r+1}$ is already $n$-reduced, the rightmost minimal poison subword must contain either $c_r$ or $c_{r+1}$. If it contains $c_r$, then $B_{r-1} \in \{-1,\, 1\}$ and $B_r \in \{c_r \pm 2k,\, c_r \pm (2k+1)\}$, and $B_{r-1}=0$, $c'_r= c_r \pm 1$ otherwise. Finally, $M=m+1$ or $M=m-1$ depending on whether $c_m$ is contained in the rightmost minimal poison subword in the sequence of rewriting rules. The sequence of rewriting rules terminates as all rewriting rules after the initial rewriting are eventually disjoint from $(c_r)$.

Proof. Let $P_\ell (X) = \sum \nolimits _{i=\ell }^m c_i X^k$. We claim that $P_\ell$ is $n$-reduced, and towards that end, we may represent $P_\ell$ as the string

\[ (c_m,\dotsc, c_\ell,\\ 0,\dotsc, 0) \]

where there are $\ell -1$ zero's at the end of the string. Since $P$ is $n$-reduced and $(c_m,\,\dotsc,\, c_\ell )$ is a substring of $(c_m,\,\dotsc,\, c_0)$, it is easy to see that Rule 1, Rule 2, and Rule 3 are satisfied for coefficients with indices between $\ell$ and $m$. Since the coefficients of $P_\ell$ with index less than $\ell$ are zero, we have that the Rule 1, Rule 2, and Rule 3 are all satisfied.

Let $m \geq t \geq i \geq \ell$, and suppose that $Q = (c_t,\,\dotsc,\, c_i)$ is a poison subword with respect to either Rule 4, Rule 5, or Rule 6. If $i>\ell$, then $(c_t,\,\dotsc,\, c_i)$ is a poison subword of $P$ with respect to Rule 4, Rule 5, or Rule 6 which is a contradiction. Thus, if $P_\ell$ contains a poison subword, it must contain the coefficient $c_\ell$.

We proceed by contradiction to demonstrate $(c_m,\, \dotsc,\, c_\ell )$ satisfies Rule 4, Rule 5, and Rule 6. We split this argument based on the rule we are trying to verify.

1. (1) Rule 4.

   If $(c_m,\,\dotsc,\, c_\ell )$ violates Rule 4, we then would have that

   \[ (c_m,\dotsc, c_\ell) ={\pm}(1, c_{m-1}^\prime,\dotsc, c^\prime_\ell) \]
   where $c_{m-j}^\prime \in \{-k+1,\,-k\}$ for $0\leq j< m-\ell$ and $c_\ell ^\prime \in \{-k,\,-k-1\}$. We have that $\operatorname {sign}(c_m \cdot c_{\ell -1}) = \operatorname {sign}(c_m \cdot 0) = \operatorname {sign}(0)$. We then have
   \[ \text{Pot}(c_m,\dotsc,c_\ell) \leq 0. \]
   However, since $(c_m,\,\dotsc,\, c_\ell )$ is a substring of $P$, we have that $(c_m,\,\dotsc,\,c_\ell )$ satisfies Rule 4. In particular, if $\operatorname {sign}(c_m \cdot c_\ell ) > 0$, then $\text {Pot}(c_m,\,\dotsc,\, c_\ell ) \geq 2$ which is a contradiction. If $\operatorname {sign}(c_m \cdot c_{\ell -1}) \leq 0$, then $\text {Pot}(c_m,\,\dotsc,\, c_\ell ) > 0$ which is also a contradiction. Thus, $P_\ell$ satisfies Rule 4.

2. (2) Rule 5.

   If $(c_m,\,\dotsc,\, c_\ell )$ violates Rule 5, we would have that $c_t \in \{k+1,\, k+2\}$ where $c_s \in \pm \{k-1,\,k\}$ for $s \neq \ell$ and $c_{\ell } \in \{k,\, k+1\}$. Since $c_{\ell -1} = 0$, we have that $\operatorname {sign}(c_m \cdot c_{\ell -1}) = 0$. Thus, we have that

   \[ \operatorname{Pot}(c_m,\dotsc, c_\ell) <{-}6. \]
   Since $(c_m,\,\dotsc,\, c_\ell )$ is a substring of $(c_m,\,\dotsc,\, c_0)$, we have that $(c_m,\,\dotsc,\, c_\ell )$ satisfies Rule 5. Hence, if $\operatorname {sign}(c_m \cdot c_{i-1}) \geq 0$, then $\text {Pot}(c_m,\,\dotsc,\, c_\ell ) > -6$ which is a contradiction. If $\operatorname {sign}(c_m \cdot c_{\ell -1}) < 0$, then $\text {Pot}(c_t,\,\dotsc,\, c_\ell ) > -4$ which is also a contradiction. Thus, $P_\ell$ must satisfy Rule 5.

3. (3) Rule 6.

   If $(c_t,\,\dotsc,\, c_\ell )$ violates Rule 6, we would have that $c_s \in \{k,\,k+1\}$ for $s \in \{t,\,\ell \}$ and $c_\ell \in \pm \{k-1,\,k\}$ otherwise. By definition of Rule 6, we have that

   \[ \operatorname{Pot}(c_t,\dotsc, c_{\ell}) \leq{-}3 - \operatorname{sign}^+(c_t \cdot c_{t+1}). \]
   However, $(c_t,\,\dotsc,\, c_\ell )$ is a substring of $P$ which implies that it satisfies Rule 6. If $\operatorname {sign}(c_t \cdot c_{\ell }) \geq 0$, then $\text {Pot}(c_j,\, \ldots,\, c_\ell ) > - 3 - \operatorname {sign}^+(c_t \cdot c_{t+1})$ which is a contradiction. If $\operatorname {sign}(c_t \cdot c_{\ell -1}) < 0$, then $\text {Pot}(c_t,\,\dotsc,\, c_{\ell }) \geq -1 - \operatorname {sign}^+(c_t \cdot c_{t+1})$ which is also a contradiction. Thus, $P_\ell$ must satisfy Rule 6.

For the second statement, we may proceed using similar arguments as for the first statement.

Proof of Theorem 24. Suppose that $F(X)$ represents $g=(x,\,t^n)$ with both non-trivial polynomial and principal parts. We first apply Proposition 23 to the principal part of $F(X)$ (namely, apply it to $X^{-1}\cdot F(X^{-1})$, we obtain $F'(X)=\sum \nolimits _{i=l<0}^{M} B_i X^i$ which represents $g$. By applying Proposition 23 to the polynomial part, we obtain

\[ G(X) = \sum_{i=0}^{M} C_i X^i + (C_{{-}1} + B_{{-}1})X^{{-}1} + \sum_{i = \ell}^{{-}2} B_i X^i. \]

If $C_{-1}=0$, then we are done. If not, we have $C_0 C_{-1}<0$ and $C_0 B_{-1}\geq 0$. Observe by Proposition 25 that $\sum \nolimits _{i = \ell }^{-2} B_i X^i$ is $n$-reduced. By Corollary 21, we have that all rewriting rules for the principal parts are disjoint from the polynomial part except $C_0$. Rewriting using Proposition 23 on the principal part, we obtain a Laurent polynomial that is $n$-reduced on the principal part, and $C_0 C_{-1}<0$ guarantees that the polynomial part is $n$-reduced as well.

Proof. This is clear from the fact that for any subword not containing $c_1$ and $c_0$, there is an identical subword in $P$. Since the subword follows all of the local and global rules applied on $P$, it never violates any of the rules. If there is no minimal poison subword of $P+1$ containing any of the coefficients, then $P+1$ is $n$-reduced.

Proof. We work out the case when the minimal poison subword for $P+1$ violates Rule 6. Denote the minimal poison subword as $(c_j,\,\dotsc,\,c_{\ell })$ Recall that Rule 6 is violated if

\[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{\ell}) <{-}2- \operatorname{sign}^+(c_j\cdot c_{j+1})- \tfrac{1}{2}\operatorname{sign}^+(c_j \cdot c_{\ell - 1}) \]

By Lemma 26, either $\ell =0$ or $\ell =1$.

1. (1) $\ell =1$. In this case, $P+1$ contains a subword $(c_j,\,\dotsc,\,c_{1},\,c_0+1)$. From $P$, the potential of the subword $(c_j,\,c_{j-1},\,\dotsc,\,c_{1})$ is

   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1}) \geq{-}2- \operatorname{sign}^+(c_j\cdot c_{j+1})- \tfrac{1}{2}\operatorname{sign}^+(c_j \cdot (c_{0})) \]
   but since it is the minimal poison subword of $P+1$, we also have
   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1}) <{-}2- \operatorname{sign}^+(c_j\cdot c_{j+1})- \tfrac{1}{2}\operatorname{sign}^+(c_j \cdot (c_{0}+1)) \]
   which can happen only when $c_0=0$ and $c_1<0$. Furthermore, we have $c_1=-k$ or $-k-1$. (Note $c_1=-k-1$ case is already included in Rule 2 violation.)

2. (2) $\ell =0$. Again, $P+1$ contains a subword $(c_j,\,\dotsc,\,c_{1},\,c_0+1)$. From $P$, the potential of the subword $(c_j,\,c_{j-1},\,\dotsc,\,c_{1},\,c_0)$ is

   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1},c_0) \geq{-}3- \operatorname{sign}^+(c_j\cdot c_{j+1}) \]
   because $c_{-1}=0$. But since it is minimal poison subword of $P+1$, we also have
   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1},c_0+1) <{-}3- \operatorname{sign}^+(c_j\cdot c_{j+1}) \]
   which happens only when $c_0>0$, that is when adding 1 to the polynomial decreases the potential by 2. If $c_0=k-1$, then the only possible value of the potential for the subword without $c_0$ is
   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1}) ={-}2 - \operatorname{sign}^+(c_j \cdot c_{j+1}), \]
   whereas if $c_0=k$,
   \[ \operatorname{Pot}(c_j,c_{j-1},\dotsc,c_{1}) \in \{{-}1 - \operatorname{sign}^+(c_j \cdot c_{j+1}),-\operatorname{sign}^+(c_j \cdot c_{j+1})\}. \]

Other cases can be worked out similarly.

Proof. This can be done by simply comparing the conditions for each sign change violation in Proposition 28. Start with an $(n+1)$-reduced polynomial

\[ P=(1,c_{m-1},\dotsc,c_1,0) \]

and suppose that $P+1$ violates Rule 4. The condition states that

\[ \operatorname{Pot}(c_{m-1},\dotsc,c_2,c_1)=1, \quad c_1=k. \]

This implies that

\[ \operatorname{Pot}(c_{m-1},\dotsc,c_2)=2 \]

which is precisely the condition for potential value change violation by Rule 4. For Rule 5, this case corresponds to 5) (ii) with potential -4, and for Rule 6, this corresponds to 6) (ii) with $Pot(A)=-1 - \operatorname {sign}^+(c_j \cdot c_{j+1})$.