in $\bigcup_{1\leq i\leq s}{\rm NTObs}(i,s)$.

By Lemma \[sec3lem10\], we can represent ${\rm o}_{i,j}(w_{i},w'_{i};w_{j},w'_{j})$ as $${\rm o}_{i,j}(w_{i},w'_{i};w_{j},w'_{j})={\rm o}_{i,s}(w_{i},w'_{i};w,w')-{\rm o}_{j,s}(w_{j},w'_{j};w,w').$$ Moreover, $S_{i,j}(w_{i},w'_{i};w_{j},w'_{j})$ has a Gröbner representations in terms of $G$ if $S_{i,s}(w_{i},w'_{i};w,w')$ and $S_{j,s}(w_{j},w'_{j};w,w')$ have Gröbner representations in terms of $G$. If ${\rm o}_{i,s}(w_{i},w'_{i};w,w')$ is an obstruction without overlap, then, by Lemma \[sec2lem8\], its S-polynomial has a Gröbner representations in terms of $G$. If it is a multiple of a non-trivial obstruction in $\bigcup_{1\leq i\leq s}{\rm NTObs}(i,s)$, then Lemma \[sec2lem8\] and Theorem \[sec2the11\] ensure that $S_{i,s}(w_{i},w'_{i};w,w')$ has a Gröbner representations in terms of $G$. By the same argument, one can show that $S_{j,s}(w_{j},w'_{j};w,w')$ has a Gröbner representations in terms of $G$. Now the conclusion follows from Proposition \[sec2pro10\] and Theorem \[sec2the11\].

We would like to mention that the Non-Commutative Backward Criterion given in Proposition \[ncBKCrit\] covers in particular all useless obstructions presented by T. Mora in [@Mo94], Lemma 5.11.

\[sec3rem13\] In order to apply Propositions \[ncMCrit\], \[ncLWCrit\], \[ncTailRed\] and \[ncBKCrit\] to remove unnecessary obstructions during the execution of the Buchberger Procedure, it is crucial to make sure that the S-polynomials of those removed obstructions have Gröbner representations.

-   Propositions \[ncMCrit\], \[ncLWCrit\] and \[ncTailRed\] remove unnecessary non-trivial obstructions, say ${\rm o}_{i,s}(w_{i},w'_{i};w_{s},w'_{s})$, from the 