use it to order obstructions. In the following, let $s\geq1$, and let $G=\{g_1,\dots,g_{s}\}\subseteq K\langle X\rangle\setminus\{0\}$ be a set of non-commutative polynomials.

\[sec3def1\] Let us define a relation $\tau$ on $\mathbb{T}(F_{s})$ as follows. For two terms $w_{1}e_{i}w'_{1},w_{2}e_{j}w'_{2}\in\mathbb{T}(F_{s})$, we let $w_{1}e_{i}w'_{1}\geq_{\tau}w_{2}e_{j}w'_{2}$ if

-   $w_{1}\lw_{\sigma}(g_{i})w'_{1}>_{\sigma}w_{2}\lw_{\sigma}(g_{j})w'_{2}$, or

-   $w_{1}\lw_{\sigma}(g_{i})w'_{1}=w_{2}\lw_{\sigma}(g_{j})w'_{2}$ and $i>j$, or

-   $w_{1}\lw_{\sigma}(g_{i})w'_{1}=w_{2}\lw_{\sigma}(g_{j})w'_{2}$ and $i=j$ and $w_{1}\geq_{\sigma}w_{2}$.

One can check that $\tau$ is a well-ordering and is compatible with scalar multiplication. The relation $\tau$ is called the *module term ordering induced by* $({\sigma},{G})$ on $\mathbb{T}(F_{s})$.

By definition, for every obstruction ${\rm o}_{i,j}(w_{i},w'_{i};w_{j},w'_{j})\in\bigcup_{1\leq i\leq j\leq s}{\rm Obs}(i,j)$, we have $w_{i}e_{i}w'_{i}<_{\tau}w_{j}e_{j}w'_{j}$. We extend the ordering $\tau$ to the set of obstructions $\bigcup_{1\leq i\leq j\leq s}{\rm Obs}(i,j)$ by committing the following slight abuse of notation.

\[sec3def2\] Let $\tau$ be the module term ordering induced by $({\sigma},{G})$ on $\mathbb{T}(F_{s})$. Let ${\rm o}_{i,j}(w_{i},w'_{i};w_{j},w'_{j}), {\rm o}_{k,l}(w_{k},w'_{k};w_{l},w'_{l})$ be two obstructions in the set $\bigcup_{1\leq i\leq j\leq s}{\rm Obs}(i,j)$. If we have $w_{j}e_{j}w'_{j}>_{\tau}w_{l}e_{l}w'_{l}$, or if we have $w_{j}e_{j}w'_{j}=w_{l}e_{l}w'_{l}$ and $w_{i}e_{i}w'_{i}\geq_{\tau}w_{k}e_{k}w'_{k}$, then we let ${\rm o}_{i,j}(w_{i},w'_{i};w_{j},w'_{j})\geq_{\tau}{\rm o}_{k,l}(w_{k},w'_{k};$ $w_{l},w'_{l})$. The ordering $\tau$ is called the ordering *induced by* $({\sigma},{G})$ on the set of obstructions.

One can verify that $\tau$ is also a well-ordering on $\bigcup_{1\leq i\leq j\leq s}{\rm Obs}(i,j)$ and compatible with scalar 