is satisfied.

-   $i>j$.

-   $i=j$ and $ww'=1$ and $w_{i}>_{\sigma}w_{j}$.

Observe that condition (a) corresponds to Lemma \[sec3lem3\].b, while condition (b) corresponds to Lemma \[sec3lem3\].c. We represent ${\rm o}_{i,s}(w_{i},w'_{i};u_{s},u'_{s})$ as $${\rm o}_{i,s}(w_{i},w'_{i};u_{s},u'_{s})=w{\rm o}_{j,s}(w_{j},w'_{j};v_{s},v'_{s})w'-{\rm o}_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i}).$$ By Lemma \[sec3lem3\].b and \[sec3lem3\].c, we have ${\rm o}_{i,s}(w_{i},w'_{i};u_{s},u'_{s})$ is strictly larger than ${\rm o}_{j,s}(w_{j},w'_{j};v_{s},v'_{s})$ and ${\rm o}_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$. Moreover, if the S-polynomials $S_{j,s}(w_{j},w'_{j};v_{s},v'_{s})$ and $S_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$ have Gröbner representations in terms of $G$, then so does $S_{i,s}(w_{i},w'_{i};u_{s},u'_{s})$. Theorem \[sec2the11\] ensures $S_{j,s}(w_{j},w'_{j};$ $v_{s},v'_{s})$ has a Gröbner representation in terms of $G$. Note that the obstruction ${\rm o}_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$ can be either a multiple of a non-trivial obstruction or an obstruction without overlap (for instance, see Example \[sec3exa4\]). If ${\rm o}_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$ is a multiple of a non-trivial obstruction, then Lemma \[sec2lem6\] and Theorem \[sec2the11\] guarantee that $S_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$ has a Gröbner representation in terms of $G$. If ${\rm o}_{j,i}(ww_{j},w'_{j}w';w_{i},w'_{i})$ is an obstruction without overlap, then, by Lemma \[sec2lem8\], its S-polynomial has a Gröbner representation in terms of $G$. Now the conclusion follows from Proposition \[sec2pro10\] and Theorem \[sec2the11\].

Next we work on detecting unnecessary obstructions in $\bigcup_{1\leq i\leq s}{\rm NTObs}(i,s)$ via obstructions in the set $\bigcup_{1\leq i\leq j\leq s-1}{\rm NTObs}(i,j)$ of previously constructed obstructions.

\[sec3lem7\] Let ${\rm o}_{j,s}(u_{j},u'_{j};w_{s},w'_{s})$ and ${\rm o}_{i,j}(w_{i},w'_{i};v_{j},v'_{j})$ 