part of a left-hand side in $\Psi$ such that
$\textup{M}_{f}(\Psi)\cap\mathbb{Z}\neq\\{0\\}$. If $\Psi$ is in increasing
form, then it is increasing for
$\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w}$,
where $\boldsymbol{z}$, $\boldsymbol{y}$ and $\boldsymbol{w}$ are the families
of variables appearing in the definition of gcd-to-div triple.

###### Proof.

For the first statement, we prove a stronger result: if $\Psi$ is not
increasing for
$\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w}$,
then there is a non-constant polynomial $f$ primitive part of a left-hand side
in $\Psi$ s.t. ${\textup{M}_{f}(\Psi)\cap\mathbb{Z}\neq\\{0\\}}$. Observe that
then, by definition of divisibility module and increasing form, $\Psi$ cannot
be in increasing form for any order; which shows the second statement in the
lemma by contrapositive.

Consider an order $x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$ of the
variables in $\Psi$ that belongs to
$\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w}$,
and suppose that $\Psi$ is not in increasing form for this order. Therefore,
there is a primitive part $f$ of a left-hand side of a divisibility in $\Psi$
such that
$\textup{M}_{f}(\Psi)\cap\mathbb{Z}[x_{1},\dots,x_{j}]\neq\mathbb{Z}f$, where
$x_{j}=\textup{LV}(f)$. Let
$g\in\textup{M}_{f}(\Psi)\cap\mathbb{Z}[x_{1},\dots,x_{j}]\setminus\mathbb{Z}f$.
We show that $g$ must be a constant polynomial. We distinguish two cases,
depending on whether the leading variable of $f$ belongs to $\boldsymbol{z}$
or to $\boldsymbol{y}$ (note that it cannot belong to $\boldsymbol{w}$, as no
left-hand sides with variables from this family exists).

case $\textup{LV}(f)$ is in $\boldsymbol{z}$.

Since $\textup{LV}(g)\preceq\textup{LV}(f)$, all variables in $g$ are from
$\boldsymbol{z}$. By Property 2 of gcd-to-div triple, each divisibility in
$\Psi$ is of the form $h(\boldsymbol{z})\mathrel{|}h^{\prime}(\boldsymbol{y})$
or of the form $h(\boldsymbol{y})\mathrel{|}h^{\prime}(\boldsymbol{w})$. By
Lemma 6, a set spanning $\textup{M}_{f}(\Psi)$ is given by $\\{f,c_{1}\cdot
g_{1},\dots,c_{m}\cdot g_{m}\\}$ where $c_{i}\in\mathbb{N}$ and $g_{i}$ is a
right-hand side of a divisibility in $\Psi$, for every $i\in[1,m]$. This means
that every $g_{i}$ has variables from $\boldsymbol{y}$ or $\boldsymbol{w}$.
Since $g$ does not have any variable from $\boldsymbol{y}$ or $\boldsymbol{w}$
and belongs to $\mathbb{Z}f$, we conclude that it must be a constant
polynomial.

case $\textup{LV}(f)$ is in $\boldsymbol{y}$.

Again from Property 2 of gcd-to-div triple, $f$ only appears as left-hand side
in divisibilities of the form $a\cdot
f(\boldsymbol{y})\mathrel{|}h(\boldsymbol{w})$, with
$a\in\mathbb{Z}\setminus\\{0\\}$. Since no non-constant polynomial
$h(\boldsymbol{w})$ appears in a left-hand side of $\Psi$, the set
$\\{f,c_{1}\cdot g_{1},\dots,c_{m}\cdot g_{m}\\}$ spanning
$\textup{M}_{f}(\Psi)$ computed via Lemma 6 is such that $c_{i}\neq 0$ if and
only if $g_{i}$ only has variables from $\boldsymbol{w}$, for every
$i\in[1,m]$. Since $\mathbin{\prec}$ belongs to
$\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w}$,
from $\textup{LV}(g)\mathbin{\prec}\textup{LV}(f)$ we then conclude that $g$
must be a constant polynomial.∎

Consider $(\Psi,\boldsymbol{u},E)\in B$. Algorithm 3 relies on Lemma 11 to
test whether $\Psi$ is increasing (line 5). If it is not, it computes the
minimum positive integer $c\in\textup{M}_{f}(\Psi)$, for some $f$ non-constant
(line 10). By definition of divisibility module, for every primitive
polynomial $f$ and polynomial $g\in\textup{M}_{f}(\Psi)$, we have that $\Psi$
entails $f\mathrel{|}g$, that is for every $\boldsymbol{a}\in\mathbb{Z}^{m}$
solution to $\Psi$, $f(\boldsymbol{a})$ divides $g(\boldsymbol{a})$; and
therefore $\Psi$ entails $f\mathrel{|}c$. We can now eliminate all variables
that occur in $f$: by definition of gcd-to-div triple, $f$ has coefficients
and constant that are all positive, and $\Psi$ is interpreted over
$\mathbb{N}$. We conclude that every solution of $\Psi$ is such that it
assigns an integer in $[0,c]$ to every variable in $f$. The for loop in line
11 iterates over the subset of these (partial) assignments satisfying
$f\mathrel{|}c$. Each of these assignments $\boldsymbol{\nu}$ yields a new
triple
$(\Psi_{\boldsymbol{\nu}},\boldsymbol{u}_{\boldsymbol{\nu}},E_{\boldsymbol{\nu}})$,
defined as in lines 12–14, which is a gcd-to-div triple thanks to the lemma
below (that follows directly from the definition of gcd-to-div triple).

######  Lemma 12.

Let $(\Psi,\boldsymbol{u},E)$ be a gcd-to-div triple, with
$\boldsymbol{u}\in\mathbb{Z}^{d}$, and $X$ be a subset of the variables
appearing in left-hand sides of $\Psi$. Consider a map $\boldsymbol{\nu}\colon
X\to\mathbb{Z}$. Let
$\Psi^{\prime}\coloneqq\Psi[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X]$,
$\boldsymbol{u}^{\prime}\in\mathbb{Z}^{d}$, and $E^{\prime}$ be the matrix
obtained from $E$ by removing the columns corresponding to variables in $X$.
The triple $(\Psi^{\prime},\boldsymbol{u}^{\prime},E^{\prime})$ is a gcd-to-
div triple.

The key equivalence, from which the correctness of the algorithm directly
stems, is:

$\\{\boldsymbol{u}+E\cdot\boldsymbol{\lambda}:\boldsymbol{\lambda}\in\mathbb{N}^{m}\text{
solution for
}\Psi\\}=\\!\bigcup_{\begin{subarray}{c}\boldsymbol{\nu}~{}\text{substitution}\\\
\text{considered in line~{}\ref{gcd-to-increasing:line-for-
loop}}\end{subarray}}\\!\\{\boldsymbol{u}_{\boldsymbol{\nu}}+E_{\boldsymbol{\nu}}\cdot\boldsymbol{\lambda}:\boldsymbol{\lambda}\in\mathbb{N}^{m-j}\text{
solution for }\Psi_{\boldsymbol{\nu}}\\},$ (10)

where $j\geq 1$ is the number of variables in $f$. The procedure adds each
triple
$(\Psi_{\boldsymbol{\nu}},\boldsymbol{u}_{\boldsymbol{\nu}},E_{\boldsymbol{\nu}})$
to the set $B$ (line 15), so that it will be tested for increasingness in a
later iteration of the while loop of line 4. Termination is guaranteed from
the fact that $f$ is non-constant and so each $\Psi_{\boldsymbol{\nu}}$ has
strictly fewer variables than $\Psi$.

######  Lemma 13.

Algorithm 3 respects its specification. On input $B$ such that, for every
$(\Psi,\boldsymbol{u},E)\in B$, $\Psi$ has at most $d$ variables and $k$ GCD
constraints, and $E$ has at most $\ell$ non-zero columns, each output triple
$(\Psi^{\prime},\boldsymbol{u}^{\prime},E^{\prime})\in C$ is such that
$\Psi^{\prime}$ has at most $d$ variables and $k$ GCD constraints,
$E^{\prime}$ has at most $\ell$ non-zero columns,
${|\mkern-2.0mu|}\Psi^{\prime}{|\mkern-2.0mu|}\leq
2^{15}(d+1)\cdot({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{7}$,
${|\mkern-2.0mu|}\boldsymbol{u}^{\prime}{|\mkern-2.0mu|}\leq(\ell+1)\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}$,
and
${|\mkern-2.0mu|}E^{\prime}{|\mkern-2.0mu|}\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$.

Above, ${|\mkern-2.0mu|}B{|\mkern-2.0mu|}$ is the maximum among
${|\mkern-2.0mu|}\Psi{|\mkern-2.0mu|}$,
${|\mkern-2.0mu|}\boldsymbol{u}{|\mkern-2.0mu|}$, and
${|\mkern-2.0mu|}E{|\mkern-2.0mu|}$, over all gcd-to-div triples
$(\Psi,\boldsymbol{u},E)\in B$. The most difficult parts of the proof are the
bounds on $\Psi^{\prime}$ and $\boldsymbol{u}^{\prime}$. These, however,
follow from the properties of gcd-to-div triples and, in particular, from the
special shape of the divisibility constraints that they allow. Together,
Lemmas 10 and 13 imply Proposition 1 in Section 1.4.

###### Proof.

The fact that Algorithm 3 respects its specification follows from the
discussion given above, and in particular from Lemma 11 and Equation 10. Let
us then focus on the bounds on an output triple
$(\Psi^{\prime},\boldsymbol{u}^{\prime},E^{\prime})$. Note that
${|\mkern-2.0mu|}B{|\mkern-2.0mu|}\geq 1$, if $B$ contains at least one
divisibility. Following the while loop of 4, there is a sequence of triples

$(\Psi_{1},\boldsymbol{u}_{1},E_{1})\ \to\
(\Psi_{2},\boldsymbol{u}_{2},E_{2})\ \to\ \dots\
\to(\Psi_{k},\boldsymbol{u}_{k},E_{k})=(\Psi^{\prime},\boldsymbol{u}^{\prime},E^{\prime}),$

where $(\Psi_{1},\boldsymbol{u}_{1},E_{1})\in B$ and for every $i\in[1,k-1]$,
the triple $(\Psi_{i+1},\boldsymbol{u}_{i+1},E_{i+1})$ is computed from
$(\Psi_{i},\boldsymbol{u}_{i},E_{i})$ following lines 8–15. In particular,
given $i\in[1,k-1]$:

  * •

there is a non-constant polynomial $\widehat{f}_{i}$ that is the part of a
left-hand side in $\Psi_{i}$ satisfying
${\textup{M}_{\widehat{f}_{i}}(\Psi_{i})\cap\mathbb{Z}\neq\\!\\{0\\}}$ and
with variables
$\widehat{\boldsymbol{\lambda}}_{i}\coloneqq(\lambda_{i,1},\dots,\lambda_{i,j_{i}})$,
and

  * •

there is a map
$\boldsymbol{\nu}_{i}:\\{\lambda_{i,1},\dots,\lambda_{i,j_{i}}\\}\to[0,\widehat{c}_{i}]$
such that
$\widehat{f}_{i}(\boldsymbol{\nu}_{i}(\widehat{\boldsymbol{\lambda}}_{i}))$
divides $\widehat{c}_{i}$, where $\widehat{c}_{i}$ is the minimum positive
integer in $\textup{M}_{\widehat{f}_{i}}(\Psi_{i})$,

such that
$\Psi_{i+1}=\Psi_{i}[\boldsymbol{\nu}_{i}(\lambda_{i,r})\mathbin{/}\lambda_{i,r}:r\in[1,j_{i}]]$,
$\boldsymbol{u}_{i+1}=\boldsymbol{u}_{i}+\sum_{r=1}^{j}\boldsymbol{\nu}_{i}(\lambda_{i,r})\cdot\boldsymbol{p}_{r}$,
where $\boldsymbol{p}_{r}$ is the column of $E_{i}$ corresponding to the
variable $\lambda_{i,r}$, and $E_{i+1}$ is obtained from $E_{i}$ by removing
the columns corresponding to variables in
$\widehat{\boldsymbol{\lambda}}_{i}$. Note that this implies that
${|\mkern-2.0mu|}E^{\prime}{|\mkern-2.0mu|}\leq{|\mkern-2.0mu|}E_{i}{|\mkern-2.0mu|}\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$
and that $E^{\prime}$ and $E_{i}$ have at most $\ell$ non-zero columns, as
required by the lemma.

We show the remaining bounds in the statement of the lemma by induction on
$i\in[1,k]$, with the induction hypothesis stating that
$(\Psi_{i},\boldsymbol{u}_{i},E_{i})$ is a gcd-to-div triple where:

  1. (A)

$\Psi_{i}$ is a system with at most $d$ variables and $k$ GCD constraints,
having the form

$\Psi_{i}=\bigwedge_{j=1}^{l}c_{j}\mathrel{|}f_{j}(\boldsymbol{y})\land\bigwedge_{j=l+1}^{n}\Big{(}z_{j}+c_{j}\mathrel{|}f_{j}(\boldsymbol{y})\land
z_{j}+c_{j}\mathrel{|}g_{j}(\boldsymbol{y})\Big{)}\land\bigwedge_{j=n+1}^{m}\Big{(}f_{j}(\boldsymbol{y})\mathrel{|}w_{j}\land
g_{j}(\boldsymbol{y})\mathrel{|}w_{j}+c_{j}\Big{)},$

where $\boldsymbol{y}$, $\boldsymbol{z}=(z_{l+1},\dots,z_{n})$ and
$\boldsymbol{w}=(w_{n+1},\dots,w_{m})$ are disjoint families of variables
(according to the definition of gcd-to-div triple), $c_{j}\in\mathbb{Z}_{+}$
for every $j\in[1,m]$, and

  2. (B)

for every $j\in[1,l]$, $c_{j}\leq
2^{15}\cdot(2+{|\mkern-2.0mu|}B{|\mkern-2.0mu|})^{7}$, and for every
$j\in[l+1,m]$, $c_{j}\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$, and

  3. (C)

for every $j\in[l+1,m]$,
$h(\boldsymbol{y})\in\\{f_{j}(\boldsymbol{y}),\,g_{j}(\boldsymbol{y})\\}$ has
variable coefficients bounded by ${|\mkern-2.0mu|}B{|\mkern-2.0mu|}$, and
constant bounded by
$(d+1-d^{\prime})\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}$, where
$d^{\prime}$ is the number of variables in $h$, and

  4. (D)

if $i\in[2,k]$, then for every $r\in[1,j_{i-1}]$, if $\lambda_{i-1,r}$ belongs
to $\boldsymbol{y}$ then
$\boldsymbol{\nu}_{i}(\lambda_{i-1,r})\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$,
and if $\lambda_{i-1,r}$ belongs to $\boldsymbol{z}$ then
$\boldsymbol{\nu}_{i}(\lambda_{i-1,r})\leq
2^{14}(2+{|\mkern-2.0mu|}B{|\mkern-2.0mu|})^{7}$.

Note that Item D implies
${|\mkern-2.0mu|}\boldsymbol{u}^{\prime}{|\mkern-2.0mu|}\leq(\ell+1)\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}$,
since all non-zero columns of $E_{1}$ correspond to variables in
$\boldsymbol{y}$, by definition of gcd-to-div triple. Items B and C imply
${|\mkern-2.0mu|}\Psi^{\prime}{|\mkern-2.0mu|}\leq
2^{15}(d+1)\cdot({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{7}$.

base case $i=1$.

In this case $(\Psi_{1},\boldsymbol{u}_{1},E_{1})\in B$ and the hypothesis
above trivially holds since $(\Psi_{1},\boldsymbol{u}_{1},E_{1})$ is a gcd-to-
div triple and Properties 2–4 ensure that $\Psi_{1}$ has the form in Item A.

induction step $i+1\geq 2$.

We assume the induction hypothesis for $(\Psi_{i},\boldsymbol{u}_{i},E_{i})$,
and establish it for $(\Psi_{i+1},\boldsymbol{u}_{i+1},E_{i+1})$. By Lemma 12,
$(\Psi_{i+1},\boldsymbol{u}_{i+1},E_{i+1})$ is a gcd-to-div triple, hence Item
A follows. So, let us focus on establishing the part of the induction
hypothesis related to the infinity norm of $\Psi_{i+1}$ and
$\boldsymbol{\nu}_{i}$ (Items B, C and D). Let $\boldsymbol{z}$,
$\boldsymbol{y}$ and $\boldsymbol{w}$ be the families of variables witnessing
that $(\Psi_{i},\boldsymbol{u}_{i},E_{i})$ is a gcd-to-div triple, according
to the definition of such triples. By Property 2, $\widehat{f}_{i}$ has
variables from either $\boldsymbol{z}$ or $\boldsymbol{y}$ (not both). We
divide the proof depending on these two cases.

case $\widehat{f}_{i}$ has only variables from $\boldsymbol{y}$.

From Property 2 of gcd-to-div triples, $\widehat{f}_{i}$ only appears as a
left-hand side in divisibilities of the form
$a\cdot\widehat{f}_{i}(\boldsymbol{y})\mathrel{|}h(\boldsymbol{w})$, with
$a\in\mathbb{Z}\setminus\\{0\\}$. From Property 4 of gcd-to-div triples
together with the fact that
$\textup{M}_{\widehat{f}_{i}}(\Psi_{i})\cap\mathbb{Z}\neq\\{0\\}$, we conclude
that there must be a variable $w$ in $\boldsymbol{w}$ and $c\in\mathbb{Z}_{+}$
such that $a_{1}\cdot\widehat{f}_{i}\mathrel{|}w$ and
$a_{2}\cdot\widehat{f}_{i}\mathrel{|}w+c$ are divisibilities in $\Psi_{i}$,
for some $a_{1},a_{2}\in\mathbb{Z}\setminus\\{0\\}$. Then,
$c\in\textup{M}_{\widehat{f}_{i}}(\Psi_{i})$ and by definition
$\widehat{c}_{i}\leq c$. By induction hypothesis (Item B),
$\widehat{c}_{i}\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$, which shows Item D
directly by definition of $\boldsymbol{\nu}_{i}$. Item B is also trivially
satisfied: since we are replacing only variables in $\boldsymbol{y}$, all
polynomials in $\Psi_{i+1}$ with variables from $\boldsymbol{z}$ or
$\boldsymbol{w}$ are polynomials in $\Psi_{i}$, and no new coefficient
$c^{\prime}$ can appear in divisibilities of the form
$c^{\prime}\mathrel{|}f(\boldsymbol{y})$.

To prove Item C, let $h^{\prime}$ be a polynomial obtained from some
$h(\boldsymbol{y})$ in $\Psi_{i}$ by evaluating each $\lambda_{i,r}$ as
$\boldsymbol{\nu}_{i}(\lambda_{i,r})$ ($r\in[1,j]$). By induction hypothesis
(Item C), $h$ has variable coefficients bounded by
${|\mkern-2.0mu|}B{|\mkern-2.0mu|}$, and constants bounded by
$(d+1-d^{\prime})\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}$, where
$d^{\prime}$ is the number of variables in $h$. Let $d^{\prime\prime}$ be the
number of variables in $h^{\prime}$. Because of the substitutions done by
$\boldsymbol{\nu}_{i}$, we conclude that the coefficients of $h^{\prime}$ are
bounded by ${|\mkern-2.0mu|}B{|\mkern-2.0mu|}$, whereas its constant is
bounded by
$(d+1-d^{\prime})\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}+(d^{\prime}-d^{\prime\prime})\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}=(d+1-d^{\prime\prime})\cdot{|\mkern-2.0mu|}B{|\mkern-2.0mu|}^{2}$.

case $\widehat{f}_{i}$ has only variables from $\boldsymbol{z}$.

In this case, $\widehat{f}_{i}$ is of the form $z+c$ for some
$c\in\mathbb{Z}_{+}$, and by Property 3 of gcd-to-div triple it appears in
exactly two divisibilities $z+c\mathrel{|}f(\boldsymbol{y})$ and
$z+c\mathrel{|}g(\boldsymbol{y})$. In order to upper bound $\widehat{c}_{i}$,
we divide the proof in two cases, depending on whether
$(\mathbb{Z}f+\mathbb{Z}g)\cap\mathbb{Z}=\\{0\\}$.

case $(\mathbb{Z}f+\mathbb{Z}g)\cap\mathbb{Z}=\\{0\\}$.

Since $\textup{M}_{\widehat{f}_{i}}(\Psi_{i})\cap\mathbb{Z}\neq\\{0\\}$, by
Properties 2 and 4 of gcd-to-div triples there must be two polynomials
$f^{\prime}(\boldsymbol{y})$ and $g^{\prime}(\boldsymbol{y})$, a variable $w$
in $\boldsymbol{w}$ and $a^{\prime},b^{\prime},c^{\prime}\in\mathbb{Z}_{+}$
such that $f^{\prime}(\boldsymbol{y})\mathrel{|}w$,
$g^{\prime}(\boldsymbol{y})\mathrel{|}w+c^{\prime}$ and $\\{a^{\prime}\cdot
f^{\prime},\,b^{\prime}\cdot g^{\prime}\\}\subseteq(\mathbb{Z}f+\mathbb{Z}g)$.
Then, by definition of divisibility module, $a^{\prime}\cdot b^{\prime}\cdot
c^{\prime}\in\textup{M}_{\widehat{f}_{i}}(\Psi_{i})$. By induction hypothesis
$c^{\prime}\leq{|\mkern-2.0mu|}B{|\mkern-2.0mu|}$ (Item B), and therefore to
find a bound on $\widehat{c}_{i}$ is suffices to bound $a^{\prime}$ and
$b^{\prime}$. Let us study the case of $a^{\prime}$ (the bound is the same for
$b^{\prime}$). The set $S\coloneqq\\{-f^{\prime},f,g\\}$ can be represented as
a matrix $A\in\mathbb{Z}^{(d+1)\times 3}$ in which each column contains the
coefficients and the constant of a distinct element of $S$. We apply
Proposition 3 on the system $A\cdot(x_{1},x_{2},x_{3})=\boldsymbol{0}$, and
conclude that $a^{\prime}$ is bounded by
$4\cdot(3\cdot\max(2,{|\mkern-2.0mu|}A{|\mkern-2.0mu|}))^{3}\leq
108\cdot({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{3}$. Therefore,
$\widehat{c}_{i}\leq 2^{14}({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{7}$.

case $(\mathbb{Z}f+\mathbb{Z}g)\cap\mathbb{Z}\neq\\{0\\}$.

In this case, we consider the set $S\coloneqq\\{f,g\\}$ and the matrix
$A\in\mathbb{Z}^{(d+1)\times 2}$ in which each column contains the
coefficients and the constant of a distinct element in $S$, with the constant
being places in the last row. To find a non-zero value
$c^{\prime}\in(\mathbb{Z}f+\mathbb{Z}g)\cap\mathbb{Z}$, we solve the system
$A\cdot(x_{1},x_{2})+x_{3}\cdot(\boldsymbol{0},1)=\boldsymbol{0}$. By
Proposition 3, $\widehat{c}_{i}\leq|c^{\prime}|\leq
4\cdot(3\cdot\max(2,{|\mkern-2.0mu|}A{|\mkern-2.0mu|}))^{3}\leq
108\cdot({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{3}$.

Therefore, $\boldsymbol{\nu}_{i}(z)\leq\widehat{c}_{i}\leq
2^{14}({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{7}$, which shows Item D of the
induction hypothesis. Item C is trivially satisfied, since
$\boldsymbol{\nu}_{i}$ replaces only the variable $z$, which does not belong
to $\boldsymbol{y}$. Item B follows from the fact that in the polynomial $z+c$
the integer $c$ is bounded by ${|\mkern-2.0mu|}B{|\mkern-2.0mu|}$ by induction
hypothesis, and therefore $\boldsymbol{\nu}(z)+c\leq
2^{15}({|\mkern-2.0mu|}B{|\mkern-2.0mu|}+1)^{7}$. ∎

###  4.2 Bound on the solutions modulo primes

Through Algorithms 2 and 3 we are able to compute from a IP-GCD system $\Phi$
a set of gcd-to-div triples $C$ such that
$\\{\boldsymbol{a}\in\mathbb{Z}^{d}:\boldsymbol{a}\text{ is a solution to
}\Phi\\}=\llbracket{C}\rrbracket$. To apply Theorem 4, what is left is to
study bounds on the solutions modulo primes in $\mathbb{P}(\Psi)$, for every
$(\Psi,\boldsymbol{u},E)\in C$.

See 5

###### Proof.

Let us assume there exists a solution
$\boldsymbol{\nu}\colon\boldsymbol{\lambda}\to\mathbb{Z}$ to
$\Psi(\boldsymbol{\lambda})$ modulo $p$. We build another solution
$\boldsymbol{\nu}^{\prime}\colon\boldsymbol{\lambda}\to\mathbb{Z}$ to
$\Psi(\boldsymbol{\lambda})$ modulo $p$ such that
${|\mkern-2.0mu|}\boldsymbol{\nu}^{\prime}(\boldsymbol{\lambda}){|\mkern-2.0mu|}\leq(d+1)\cdot{|\mkern-2.0mu|}\Psi{|\mkern-2.0mu|}^{3}p^{2}$.
According to Properties 2–4 of gcd-to-div triples, the formula $\Psi$ is of
the form:

$\Psi=\bigwedge_{i=1}^{l}c_{i}\mathrel{|}f_{i}(\boldsymbol{y})\land\bigwedge_{i=l+1}^{n}\Big{(}z_{i}+c_{i}\mathrel{|}f_{i}(\boldsymbol{y})\land
z_{i}+c_{i}\mathrel{|}g_{i}(\boldsymbol{y})\Big{)}\land\bigwedge_{i=n+1}^{m}\Big{(}f_{i}(\boldsymbol{y})\mathrel{|}w_{i}\land
g_{i}(\boldsymbol{y})\mathrel{|}w_{i}+c_{i}\Big{)},$

where $\boldsymbol{y}$, $\boldsymbol{z}=(z_{l+1},\dots,z_{n})$ and
$\boldsymbol{w}=(w_{n+1},\dots,w_{m})$ are disjoint families of variables, and
$c_{i}\in\mathbb{Z}_{+}$ for every $i\in[1,m]$. Recall that the variables
$z_{i}$ ($i\in[l+1,n]$) are all distinct, and the same holds true for the
variables $w_{i}$ $(i\in[n+1,m]$). We define $\mu_{i}\coloneqq v_{p}(c_{i})$,
$\mu\coloneqq\max_{i=1}^{m}\mu_{i}$, and $\boldsymbol{\nu}^{\prime}$ as:

$\displaystyle\boldsymbol{\nu}^{\prime}(x)\coloneqq\\!\begin{cases}(\boldsymbol{\nu}(x)\text{
modulo }p^{\mu})&\text{if }x\text{ belongs to }\boldsymbol{y},\\\ 1&\text{if
}x=z_{i}\text{ for some }i\in[l+1,n]\text{ and }p\text{ divides }c_{i},\\\
0&\text{if }x=z_{i}\text{ for some }i\in[l+1,n]\text{ and }p\text{ does not
divide }c_{i},\\\
p^{\mu+1}g_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))\,{-}\,c_{i}&\text{if
}x=w_{i}\text{ for some }i\,{\in}\,[n\,{+}\,1,m]\text{ and
}p^{\mu_{i}+1}\,\text{does not
divide}\,f_{i}(\boldsymbol{\nu}(\boldsymbol{y})),\\\
p^{\mu+1}f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))&\text{otherwise
}(x=w_{i}\text{ for some }i\in[n+1,m]).\\\ \end{cases}$

Note that $\boldsymbol{\nu}^{\prime}$ is defined recursively in the last two
cases; this recursion is on variables from $\boldsymbol{y}$ and thus
$\boldsymbol{\nu}^{\prime}$ is well-defined. By definition,
$p^{\mu+1}\leq{|\mkern-2.0mu|}\Psi{|\mkern-2.0mu|}\cdot p$, and therefore
${|\mkern-2.0mu|}\boldsymbol{\nu}^{\prime}(x){|\mkern-2.0mu|}\leq(d+1)\cdot{|\mkern-2.0mu|}\Psi{|\mkern-2.0mu|}^{3}p^{2}$
for every variable $x$ in $\boldsymbol{\lambda}$. To conclude the proof, let
us show that $\boldsymbol{\nu}^{\prime}$ is a solution for $\Psi$ modulo $p$.
The fact that $f(\boldsymbol{\nu}^{\prime}(\boldsymbol{\lambda}))\neq 0$ for
every polynomial $f$ in the left-hand side of a divisibility in $\Psi$ stems
from $\boldsymbol{\nu}^{\prime}$ being defined to be non-negative for every
variable in $\boldsymbol{z}$ and $\boldsymbol{y}$, and $f$ having a positive
constant by Property 2 of gcd-to-div triples. So, we focus on showing that
$v_{p}(f(\boldsymbol{\nu}^{\prime}(\boldsymbol{\lambda})))\leq
v_{p}(g(\boldsymbol{\nu}^{\prime}(\boldsymbol{\lambda})))$ for every
divisibility $f\mathrel{|}g$ in $\Psi$.

Let $i\in[1,l]$, and consider $c_{i}\mathrel{|}f_{i}(\boldsymbol{y})$. By
definition of $\boldsymbol{\nu}^{\prime}$,
${f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))\equiv
f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))\pmod{p^{\mu+1}}}$, and therefore
$v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))=\min(\mu+1,v_{p}(f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))))$.
By definition of $\mu$, we have $c_{i}\not\equiv 0\pmod{p^{\mu+1}}$, i.e.,
$v_{p}(c_{i})<\mu+1$. We conclude that $v_{p}(c_{i})\leq
v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))$.

Let $i\in[l+1,n]$, and consider the divisibilities
$z_{i}+c_{i}\mathrel{|}f_{i}(\boldsymbol{y})$ and
$z_{i}+c_{i}\mathrel{|}g_{i}(\boldsymbol{y})$. By definition of
$\boldsymbol{\nu}^{\prime}$ we have
$v_{p}(\boldsymbol{\nu}^{\prime}(z_{i})+c_{i})=0$, and so
$v_{p}(\boldsymbol{\nu}^{\prime}(z_{i})+c_{i})\leq
v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))$ and
$v_{p}(\boldsymbol{\nu}^{\prime}(z_{i})+c_{i})\leq
v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))$.

Let $i\in[n+1,m]$. Assume first that $p^{\mu_{i}+1}$ does not divide
$f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))$, and so $\boldsymbol{\nu}^{\prime}$
is defined so that
$\boldsymbol{\nu}^{\prime}(w_{i})=p^{\mu+1}g_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))-c_{i}$.
The divisibility $g_{i}(\boldsymbol{y})\mathrel{|}w_{i}+c$ is trivially
satisfied by $\boldsymbol{\nu}^{\prime}$ over the integers, and thus also
modulo $p$. By definition of $\boldsymbol{\nu}^{\prime}$ we have
${f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))\equiv
f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))\pmod{p^{\mu+1}}}$ and therefore
$p^{\mu_{i}+1}$ does not divide
$f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))$. By definition of
$\mu_{i}$, this implies
${v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))\leq v_{p}(c_{i})}$.
From the definition of $\mu$,
$v_{p}(p^{\mu+1}g_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))>v_{p}(c_{i})$
and therefore $v_{p}(\boldsymbol{\nu}^{\prime}(w_{i}))=v_{p}(c_{i})$, which
yield $v_{p}(f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))\leq
v_{p}(\boldsymbol{\nu}^{\prime}(w_{i}))$. Let us now assume that
$p^{\mu_{i}+1}$ divides $f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))$, and so
$\boldsymbol{\nu}^{\prime}$ is defined so that
$\boldsymbol{\nu}^{\prime}(w_{i})=p^{\mu+1}f_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))$.
Clearly, the divisibility $f_{i}(\boldsymbol{y})\mathrel{|}w_{i}$ is satisfied
by $\boldsymbol{\nu}^{\prime}$ over the integers, and thus also modulo $p$.
Since $\boldsymbol{\nu}$ is a solution for $\Psi$ modulo $p$, and $p^{\mu+1}$
divides $f_{i}(\boldsymbol{\nu}(\boldsymbol{y}))$, we conclude that
$p^{\mu+1}$ divides $\boldsymbol{\nu}(w_{i})$. Then, by definition of $\mu$,
$v_{p}(\boldsymbol{\nu}(w_{i}))>v_{p}(c_{i})$ and therefore
$v_{p}(g_{i}(\boldsymbol{\nu}(\boldsymbol{y})))\leq
v_{p}(\boldsymbol{\nu}(w_{i})+c_{i})=v_{p}(c_{i})$. By definition of
$\boldsymbol{\nu}^{\prime}$,
${g_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y}))\equiv
g_{i}(\boldsymbol{\nu}(\boldsymbol{y}))\pmod{p^{\mu+1}}}$ and
${v_{p}(\boldsymbol{\nu}^{\prime}(w_{i})+c_{i})=v_{p}(c_{i})}$. We conclude
that ${v_{p}(g_{i}(\boldsymbol{\nu}^{\prime}(\boldsymbol{y})))\leq
v_{p}(\boldsymbol{\nu}^{\prime}(w_{i})+c_{i})}$. ∎

###  4.3 Proof of Theorem 1

Thanks to Lemmas 4, 10, 13 and 5, we obtain the part of Theorem 1 not
concerning optimization as a corollary of Theorem 4.

######  Corollary 1.

Each feasible IP-GCD system has a solution of polynomial bit length.

Let us now discuss the related integer programming optimization problem.
Consider an IP-GCD system $\Phi(\boldsymbol{x})$ and the problem of minimizing
(or maximizing) a linear objective $\boldsymbol{c}^{\intercal}\boldsymbol{x}$
subject to $\Phi(\boldsymbol{x})$. We apply Lemmas 10 and 13 on
$\Phi(\boldsymbol{x})$ to obtain a set $C$ of gcd-to-div triples only
featuring $3$-increasing systems of divisibility constraints , and with
$\\{\boldsymbol{a}\in\mathbb{Z}^{d}:\boldsymbol{a}\text{ solution to
}\Phi\\}=\llbracket{C}\rrbracket$. We show the following characterization that
implies the optimization part of Theorem 1:

  1. I.

if for every $(\Psi,\boldsymbol{u},E)\in C$, $\Psi$ is unsatisfiable over
$\mathbb{N}$, then $\Phi$ is unsatisfiable;

  2. II.

else, if there is $(\Psi,\boldsymbol{u},E)\in C$ such that $\Psi$ is
satisfiable over $\mathbb{N}$ and the linear polynomial
${\boldsymbol{c}^{\intercal}(\boldsymbol{u}+E\cdot\boldsymbol{\lambda})}$ has
a variable in $\boldsymbol{\lambda}$ with strictly negative (resp. positive)
coefficient, then an optimal solution minimizing (resp. maximizing)
$\boldsymbol{c}^{\intercal}\boldsymbol{x}$ subject to $\Phi(\boldsymbol{x})$
does not exist;

  3. III.

else, an optimal solution does exist, and in particular one with polynomial
bit length with respect to $\langle\Phi\rangle$ and
$\langle\boldsymbol{c}\rangle$.

Item I follows directly from the equivalence
$\\{\boldsymbol{a}\in\mathbb{Z}^{d}:\boldsymbol{a}\text{ solution ot
}\Phi\\}=\llbracket{C}\rrbracket$. Let us focus on Item II, which we show for
the case of minimization (the case of maximization being analogous). Consider
a triple $(\Psi,\boldsymbol{u},E)\in C$ such that $\Psi$ is satisfiable and
the linear polynomial
$f(\boldsymbol{\lambda})\coloneqq\boldsymbol{c}^{\intercal}(\boldsymbol{u}+E\cdot\boldsymbol{\lambda})$
has a variable in $\boldsymbol{\lambda}$ with strictly negative coefficient.
Let $\boldsymbol{z}$, $\boldsymbol{y}$ and $\boldsymbol{w}$ be the disjoint
families of variable witnessing the fact that $(\Psi,\boldsymbol{u},E)$ is a
gcd-to-div triple, according to the definition of such triples. By Lemma 11,
$\Psi$ is increasing for
$\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w}$,
and from Property 5 of gcd-to-div triples, all variables appearing in
$f(\boldsymbol{\lambda})$ with a non-zero coefficient are from
$\boldsymbol{y}$. Let $\widehat{y}$ be a variable appearing in $f$ with a
negative coefficient, and consider an order
$(\mathbin{\prec})\in(\boldsymbol{z}\mathbin{\prec}\boldsymbol{y}\mathbin{\prec}\boldsymbol{w})$
for which $\widehat{y}$ is the largest of the variables appearing in
$\boldsymbol{y}$. Since $\Psi$ is satisfiable over $\mathbb{N}$, it is
satisfiable modulo every prime in $\mathbb{P}(\Psi)$, and we can apply
Algorithm 1 to compute a solution $\boldsymbol{\nu}$ over $\mathbb{N}$
satisfying the property highlighted in Remark 1: the formula
$\Psi[\boldsymbol{\nu}(x)\mathbin{/}x:x\mathbin{\prec}\widehat{y}\,]$ has a
solution for infinitely many positive values of $\widehat{y}$. Since
$\widehat{y}$ is the largest (for $\mathbin{\prec}$) variable appearing in
$f$, and its coefficient in $f$ is negative, we conclude that
$\min\\{f(\boldsymbol{\lambda})\in\mathbb{Z}:\boldsymbol{\lambda}\text{ is a
solution to }\Psi\\}$ is undefined, which in turn implies that an optimal
solution minimizing $\boldsymbol{c}^{\intercal}\boldsymbol{x}$ subject to
$\Phi(\boldsymbol{x})$ does not exist.

Lastly, let us consider Item III. Again we focus on the case of minimization.
Below, let $C^{\prime}\coloneqq\\{(\Psi,\boldsymbol{u},E)\in C:\Psi\text{ is
satisfiable over }\mathbb{N}\\}$ and note that
$\\{\boldsymbol{x}\in\mathbb{Z}^{d}:\Phi(\boldsymbol{x})\\}=\llbracket{C^{\prime}}\rrbracket$.
As Items I and II do not hold, $C^{\prime}\neq\emptyset$ and every gcd-to-div
triple $(\Psi,\boldsymbol{u},E)\in C^{\prime}$ is such that the linear
polynomial
$\boldsymbol{c}^{\intercal}(\boldsymbol{u}+E\cdot\boldsymbol{\lambda})$ only
has non-negative coefficients. Since the variables $\boldsymbol{\lambda}$ are
interpreted over $\mathbb{N}$, this means that
$\ell\coloneqq\min\\{\boldsymbol{c}^{\intercal}\boldsymbol{u}:(\Psi,\boldsymbol{u},E)\in
C^{\prime}\\}$ is a lower bound to the values that
$\boldsymbol{c}^{\intercal}\boldsymbol{x}$ can take when $\boldsymbol{x}$ is a
solution to $\Phi$; i.e., the optimal solution exists. Lemmas 10 and 13 ensure
that the lower bound $\ell$ has polynomial bit length with respect to
$\langle\Phi\rangle$ and $\langle\boldsymbol{c}\rangle$. We also have an upper
bound $u$ to the optimal solution: it suffices to take the minimum of the
values $(\boldsymbol{u}+E\cdot\boldsymbol{\lambda})$, where
$(\Psi,\boldsymbol{u},E)\in C^{\prime}$ and $\boldsymbol{\lambda}$ is the
positive integer solution to $\Psi$ computed with Algorithm 1 using the
solutions modulo $p\in\mathbb{P}(\Psi)$ of Lemma 5. Again, $u$ has polynomial
bit length with respect to $\langle\Phi\rangle$ and
$\langle\boldsymbol{c}\rangle$, thanks to Lemmas 4, 10 and 13, and Theorem 4.
Item III then follows by reduction from the feasibility problem of IP-GCD
systems: it suffices to find the minimal $v\in[\ell,u]$ such that the IP-GCD
system
$\Phi_{v}(\boldsymbol{x})\coloneqq\Phi(\boldsymbol{x})\land(\boldsymbol{c}^{\intercal}\boldsymbol{x}\leq
v)$ is feasible. Since every $v\in[\ell,u]$ is of polynomial bit length, by
Corollary 1 if $\Phi_{v}(\boldsymbol{x})$ is satisfiable, then it has a
solution $\boldsymbol{x}\in\mathbb{Z}^{d}$ such that
$\langle\boldsymbol{x}\rangle\leq\mathrm{poly}(\langle\Phi\rangle,\langle\boldsymbol{c}\rangle)$.

##  Appendix A Lemma 1: proof of 1

In this appendix, we present the technical manipulation yielding 1, hence
finishing the proof of Lemma 1. Below, $\mu$ and $\omega$ stand for the Möbius
function and the prime omega function, respectively. Recall that
$\mu(n)=(-1)^{\omega(n)}$ and $\omega(n)=\\#\mathbb{P}(n)$, for every
$n\in\mathbb{Z}_{+}$.

######  Proposition 4 (Möbius inversion [7, Theorem 266]).

Consider two functions $f,g\colon\mathbb{Z}_{+}\to\mathbb{R}$ such that for
every $n\in\mathbb{Z}_{+}$, $f(n)=\sum_{d\in\textup{div}(n)}g(d)$. For every
$m\in\mathbb{Z}_{+}$,
$g(m)=\sum_{d\in\textup{div}(m)}f(d)\cdot\mu(\frac{m}{d})$.

######  Proposition 5 (Möbius sums [7, Theorem 263]).

For $n\in\mathbb{Z}_{+}$ greater than $1$,
$\sum_{s\in\textup{div}(n)}\mu(s)=0$.

The following lemma tells us what to expect when we truncate the sum of the
previous proposition so that it only considers elements with at most $\ell$
divisors.

######  Lemma 14.

Let $n,\ell\,{\in}\,\mathbb{N}$ with $n$ square-free. If $\omega(n)>\ell$ then
$\sum_{r\in\textup{div}(n),\,\omega(r)\leq\ell}\,\mu(r)=(-1)^{\ell}{\omega(n)-1\choose\ell}$.

###### Proof.

We write LHS (resp. RHS) for the left-hand (resp. right-hand) side of the
equivalence in the statement. Note that $\omega(n)>\ell$ implies $n\geq 1$.
The proof is by induction on $\ell$.

#### Base case: $\ell=0$:

In this case, $\text{LHS}=\mu(1)=1=(-1)^{0}{\omega(n)-1\choose 0}=\text{RHS}$.

#### Induction step: $\ell\geq 1$:

We have,

LHS
$\displaystyle=\sum_{r\in\textup{div}(n),\,\omega(r)<\ell}\mu(r)+\sum_{s\in\textup{div}(n),\,\omega(r)=\ell}\mu(s)$
$\displaystyle=(-1)^{\ell-1}{\omega(n)-1\choose\ell-1}+\sum_{s\in\textup{div}(n),\,\omega(r)=\ell}\mu(s)$
$\displaystyle\begin{aligned} \text{by induction hypothesis;}\\\ \text{recall
$\omega(n)>\ell$}\end{aligned}$
$\displaystyle=(-1)^{\ell-1}\left({\omega(n)-1\choose\ell-1}-\sum_{r\in\textup{div}(n),\,\omega(r)=\ell}1\right)$
since $\mu(r)=(-1)^{\ell}$ iff $\omega(r)=\ell$
$\displaystyle=(-1)^{\ell-1}\left({\omega(n)-1\choose\ell-1}-{\omega(n)\choose\ell}\right)$
from $n$ square-free
$\displaystyle=(-1)^{\ell}{\omega(n)-1\choose\ell}=\text{RHS}$ Pascal’s rule.

We are now ready to prove 1:

See 1

Let us recall the hypothesis under which this claim must be proved:
$\ell\in\mathbb{N}_{+}$ is odd, $d\geq 1$, $Q$ is a non-empty finite set of
primes, $Q(\ell)\coloneqq\\{r\in\textup{div}(\Pi Q):\omega(r)\leq\ell\\}$, $m$
is a multiplicative function such that $m(q)\leq q-1$ and $m(q)\leq d$ on all
$q\in Q$, and $W_{m}(Q)\coloneqq\prod_{q\in Q}\left(1-\frac{m(q)}{q}\right)$.

###### Proof.

We start by defining the truncated Möbius function $\mu_{\ell}$ and its
companion function $\psi_{\ell}$:

$\mu_{\ell}(x)\coloneqq\begin{cases}\mu(x)&\text{if $\omega(x)\leq\ell$}\\\
0&\text{otherwise}\end{cases}\qquad\text{ and
}\qquad\psi_{\ell}(x)\coloneqq\sum_{r\in\textup{div}(x)}\mu_{\ell}(x).$

The proof proceeds by performing two term manipulations. In the first one, we
use the fact that $m$ is multiplicative, together with properties of the
Möbius function (e.g. Proposition 4), to show that

$\sum_{r\in Q(\ell)}\frac{\mu(r)\cdot
m(r)}{r}=W_{m}(Q)\cdot\left(1+\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi
Q)\\\ \omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right).$ (11)

In the second manipulation, we look at the sum $\sum_{s\in\textup{div}(\Pi
Q)\setminus\\{1\\}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}$ from the equation above, and (also thanks to Lemma 14)
bound it in absolute terms as follows:

$\left|\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right|\leq\left(\frac{e\cdot\alpha}{\ell}\right)^{\ell}\cdot\alpha\cdot
e^{\alpha},\ \text{ where }\alpha\coloneqq(d+1)^{2}(2+\ln\ln(\\#Q+1)).$ (12)

1 follows directly from Equation 11 and Equation 12. Note that these equations
can be used to also establish the upper bound to $\sum_{r\in
Q(\ell)}\frac{\mu(r)\cdot m(r)}{r}$ required for the upper bound of Lemma 1.

#### Manipulation resulting in Equation 11:

$\displaystyle\ \ \sum_{r\in Q(\ell)}\frac{\mu(r)\cdot m(r)}{r}$
$\displaystyle=\,$ $\displaystyle\sum_{r\in\textup{div}(\Pi
Q)}\frac{\mu_{\ell}(r)\cdot m(r)}{r}$ by def. of $\mu_{\ell}$
$\displaystyle=\,$ $\displaystyle\sum_{r\in\textup{div}(\Pi
Q)}\frac{\left(\sum_{s\in\textup{div}(r)}\psi_{\ell}(s)\cdot\mu\left(\frac{r}{s}\right)\right)\cdot
m(r)}{r}$ by Proposition 4 $\displaystyle=\,$
$\displaystyle\sum_{r\in\textup{div}(\Pi
Q)}\sum_{s\in\textup{div}(r)}\frac{\psi_{\ell}(s)\cdot\mu\left(\frac{r}{s}\right)\cdot
m(r)}{r}$ $\displaystyle=\,$ $\displaystyle\sum_{s\in\textup{div}(\Pi
Q)}\sum_{r\in\textup{div}\left(\frac{\Pi
Q}{s}\right)}\frac{\psi_{\ell}(s)\cdot\mu(r)\cdot m(r\cdot s)}{r\cdot s}$
$\displaystyle\begin{aligned} \text{invert summations using the}\\\
\text{change of variable $r\leftarrow r\cdot s$}\end{aligned}$
$\displaystyle=\,$ $\displaystyle\sum_{s\in\textup{div}(\Pi
Q)}\frac{\psi_{\ell}(s)\cdot
m(s)}{s}\cdot\sum_{r\in\textup{div}\left(\frac{\Pi
Q}{s}\right)}\frac{\mu(r)\cdot m(r)}{r}$ multiplicity of $m$
$\displaystyle=\,$ $\displaystyle\sum_{s\in\textup{div}(\Pi
Q)}\frac{\psi_{\ell}(s)\cdot m(s)}{s}\cdot\prod_{q\in
Q\setminus\textup{div}(s)}\left(1+\frac{\mu(q)\cdot m(q)}{q}\right)$
$\displaystyle\begin{aligned} \text{multiplicity of~{}$\mu$ and~{}$m$;}\\\
\text{factorization thanks to $r$ being}\\\ \text{square-free, for all
$r\in\textup{div}\\!\textstyle\left(\frac{\Pi Q}{s}\right)$}\end{aligned}$
$\displaystyle=\,$ $\displaystyle\sum_{s\in\textup{div}(\Pi
Q)}\frac{\psi_{\ell}(s)\cdot m(s)}{s}\cdot\frac{\prod_{q\in
Q}\left(1-\frac{m(q)}{q}\right)}{\prod_{q\in\mathbb{P}(s)}\left(1-\frac{m(q)}{q}\right)}$
$\displaystyle\begin{aligned} \text{$\mu(q)=-1$ for $q$ prime}\\\ \text{and
simple manipulation}\end{aligned}$ $\displaystyle=\,$
$\displaystyle\sum_{s\in\textup{div}(\Pi Q)}\frac{\psi_{\ell}(s)\cdot
m(s)}{s}\cdot\frac{W_{m}(Q)}{W_{m}(\mathbb{P}(s))}$ by def. of $W_{m}$
$\displaystyle=\,$ $\displaystyle\,W_{m}(Q)\cdot\sum_{s\in\textup{div}(\Pi
Q)}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot W_{m}(\mathbb{P}(s))}$
$\displaystyle=\,$ $\displaystyle\,W_{m}(Q)\cdot\left(\sum_{s\in
Q(\ell)}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}+\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right)$ $\displaystyle\begin{aligned} \text{split
depending on $\omega(s)\leq\ell$,}\\\ \text{and by
def.~{}of~{}$Q(\ell)$}\end{aligned}$ $\displaystyle=\,$
$\displaystyle\,W_{m}(Q)\cdot\left(\sum_{s\in
Q(\ell)}\frac{\left(\sum_{r\in\textup{div}(s)}\mu(r)\right)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}+\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right)$ def. of $\psi_{\ell}$ $\displaystyle=\,$
$\displaystyle\,W_{m}(Q)\cdot\left(1+\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi
Q)\\\ \omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right)$ $\displaystyle\begin{aligned} \text{in the left
summation:}\\\ \text{for $s=1$ the addend is $1$,}\\\ \text{and for $s>1$ the
addend is $0$}\\\ \text{by~{}\lx@cref{creftypecap~refnum}{lemma:Mobius-
sums}.}\end{aligned}$

#### Manipulation resulting in Equation 12:

$\displaystyle\left|\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right|\leq\,$
$\displaystyle\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}{\omega(s)-1\choose\ell}\cdot\frac{m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}$ by Lemma 14 and def. of $\psi_{\ell}$
$\displaystyle=\,$
$\displaystyle\sum_{k=\ell+1}^{\\#Q}\left(\binom{k-1}{\ell}\cdot\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi
Q)\\\ \omega(s)=k\end{subarray}}\frac{m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right)$ split on the value of $\omega(s)$.

We focus on the summation $\sum_{s\in\textup{div}(\Pi
Q),\,\omega(s)=k}\frac{m(s)}{s\cdot W_{m}(\mathbb{P}(s))}$. Since the function
$m$ is multiplicative, and similarly $W_{m}(A\cup B)=W_{m}(A)\cdot W_{m}(B)$
for $A,B$ disjoint finite sets of primes (and $W_{m}(\emptyset)=1$ by
definition), for $k\geq 1$ we have:

$\displaystyle\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)=k\end{subarray}}\frac{m(s)}{s\cdot W_{m}(\mathbb{P}(s))}$
$\displaystyle=\sum_{q_{1}<...<q_{k}\in
Q}\left(\prod_{i=1}^{k}\frac{m(q_{i})}{q_{i}\cdot
W_{m}(\\{q_{i}\\})}\right)\leq\frac{1}{k!}\sum_{q_{1},...,q_{k}\in
Q}\left(\prod_{i=1}^{k}\frac{m(q_{i})}{q_{i}\cdot W_{m}(\\{q_{i}\\})}\right)$
$\displaystyle=\frac{1}{k!}\left(\sum_{q\in Q}\frac{m(q)}{q\cdot
W_{m}(\\{q\\})}\right)^{k}=\frac{1}{k!}\left(\sum_{q\in
Q}\frac{m(q)}{q-m(q)}\right)^{k}.$

We further analyse the summation $\sum_{q\in Q}\frac{m(q)}{q-m(q)}$. Below, we
write $Q_{d+1}$ for the set of the first $\min(\\#Q,d+1)$ many primes in $Q$
(recall $d\geq 1$), and denote by $p_{i}$ the $i$-th prime.

$\displaystyle\sum_{q\in Q}\frac{m(q)}{q-m(q)}$ $\displaystyle=\sum_{q\in
Q_{d+1}}\frac{m(q)}{q-m(q)}+\sum_{q\in Q\setminus Q_{d+1}}\frac{m(q)}{q-m(q)}$
$\displaystyle\leq\sum_{q\in Q_{d+1}}d+\sum_{q\in Q\setminus
Q_{d+1}}\frac{m(q)}{q-m(q)}$ $\displaystyle\begin{aligned} \text{since
}m(q)\leq d\\\ \text{and }q-m(q)\geq 1\end{aligned}$ $\displaystyle\leq
d\cdot(d+1)+\sum_{q\in Q\setminus Q_{d+1}}\frac{d}{q-d}$ $m(q)\leq d<q$, for
all $q\in Q\setminus Q_{d+1}$ $\displaystyle\leq
d\cdot(d+1)+\sum_{i=d+2}^{\\#Q}\frac{d}{p_{i}-d}$
$\displaystyle\begin{aligned} \text{def.~{}of~{}$Q\setminus Q_{d+1}$}\\\
\text{and $p_{i}>d$ for $i\geq d+2$}\end{aligned}$ $\displaystyle\leq
d\cdot(d+1)+d\cdot\sum_{i=d+2}^{\\#Q}\frac{1}{(i\ln i)-d}$
$\displaystyle\begin{aligned} p_{i}\geq i\ln i\text{
\cite[cite]{[\@@bibref{Number}{Rosser39}{}{}]}}\\\ \text{and $i\ln i>d$ for
$i\geq d+2$}\end{aligned}$ $\displaystyle\leq
d\cdot(d+1)+d\cdot(d+1)\sum_{i=d+2}^{\\#Q}\frac{1}{i\ln i}$
$\displaystyle\begin{aligned} \text{since }\ \frac{1}{x\ln
x-y}\leq\frac{y+1}{x\ln x}\\\ \text{for all }x\geq 3\text{ and }0\leq y\leq
x-1\end{aligned}$ $\displaystyle\leq
d\cdot(d+1)\cdot\Big{(}1+\sum_{i=3}^{\\#Q}\frac{1}{i\ln i}\Big{)}$
$\displaystyle\leq d\cdot(d+1)\cdot\Big{(}1+\int_{2}^{\\#Q+1}\frac{1}{x\ln
x}\textup{d}x\Big{)}$ $\displaystyle\begin{aligned} \text{Riemann over-
approximation}\\\ \text{note: $\\#Q+1\geq 2$}\end{aligned}$ $\displaystyle\leq
d\cdot(d+1)\cdot(1+\ln\ln(\\#Q+1)-\ln\ln 2)$
$\displaystyle\leq(d+1)^{2}(2+\ln\ln(\\#Q+1))\ =\ \alpha.$

We combine this bound with the previous two to obtain complete the proof of
Equation 12:

$\displaystyle\left|\sum_{\begin{subarray}{c}s\in\textup{div}(\Pi Q)\\\
\omega(s)>\ell\end{subarray}}\frac{\psi_{\ell}(s)\cdot m(s)}{s\cdot
W_{m}(\mathbb{P}(s))}\right|$
$\displaystyle\leq\sum_{k=\ell+1}^{\\#Q}\left(\binom{k-1}{\ell}\cdot\frac{1}{k!}\cdot\alpha^{k}\right)$
$\displaystyle=\sum_{j=0}^{\\#Q-\ell-1}\left(\binom{\ell+j}{\ell}\cdot\frac{1}{(\ell+1+j)!}\cdot\alpha^{\ell+1+j}\right)$
$\displaystyle\begin{aligned} \text{change of variable}\\\
k\leftarrow\ell+1+j\end{aligned}$
$\displaystyle=\sum_{j=0}^{\\#Q-\ell-1}\left(\frac{(\ell+j)!}{\ell!\cdot
j!\cdot(\ell+1+j)!}\cdot\alpha^{\ell+1+j}\right)$
$\displaystyle\leq\frac{\alpha^{\ell+1}}{\ell!}\cdot\sum_{j=0}^{\infty}\frac{\alpha^{j}}{j!}$
$\displaystyle\begin{aligned} \text{note: all terms in the}\\\ \text{summation
are non-negative}\end{aligned}$
$\displaystyle\leq\frac{\alpha^{\ell+1}}{\ell!}\cdot e^{\alpha}$
$\displaystyle\begin{aligned} \text{def.~{}of $e^{x}$ as a series}\\\
\text{i.e.,~{}$\textstyle
e^{x}=\sum_{i=0}^{\infty}\frac{x^{i}}{i!}$}\end{aligned}$
$\displaystyle\leq\left(\frac{e\cdot\alpha}{\ell}\right)^{\ell}\cdot\alpha\cdot
e^{\alpha}$ $\displaystyle\text{from }x!\geq\frac{x^{x}}{e^{x}}.$

This completes the proof of 1. ∎

##  Appendix B Theorem 3: proofs of 2 and 3

The mathematical objects appearing in the statements of the two claims below
are defined in the proof of Theorem 3 and the statement of Lemma 1; see
Section 2.

See 2

###### Proof.

Recall that $A=[k,k+z]\cap S_{M}$, and so $A\cap S_{\alpha,r}=[k,k+z]\cap
S_{M}\cap S_{\alpha,r}$. Since that elements in $M\cup Q$ are pairwise coprime
and $M\cap Q=\emptyset$, we can apply the CRT and conclude that $S_{M}\cap
S_{\alpha,r}$ is an arithmetic progression with period $r\cdot\Pi M$. Let $u$
be the largest element of $S_{M}\cap S_{\alpha,r}$ that is strictly smaller
than $k$. By definition of $u$ and from the fact that $S_{M}\cap S_{\alpha,r}$
has period $r\cdot\Pi M$, we get $\\#(A\cap
S_{\alpha,r})=\left\lfloor\frac{k+z-u}{r\cdot\Pi M}\right\rfloor$. Similarly,
because $S_{M}$ is periodic in $\Pi M$, $\left\lfloor\frac{k+z-u}{\Pi
M}\right\rfloor$ is over counting $\\#A$ by at most $r-1$, i.e., there is
$\tau_{\alpha,r}\in[0,r-1]$ such that $\\#A=\left\lfloor\frac{k+z-u}{\Pi
M}\right\rfloor-\tau_{\alpha,r}$. Since
$\left\lfloor\frac{a}{b}\right\rfloor=\left\lfloor\frac{\left\lfloor
a\right\rfloor}{b}\right\rfloor$ for every $a\in\mathbb{R}$ and
$b\in\mathbb{Z}_{+}$, we get $\\#(A\cap
S_{\alpha,r})=\left\lfloor\frac{1}{r}\cdot(\\#A+\tau_{\alpha,r})\right\rfloor$.
With a simple manipulation using $\left\lfloor a\right\rfloor+\left\lfloor
b\right\rfloor\leq\left\lfloor a+b\right\rfloor\leq\left\lfloor
a\right\rfloor+\left\lfloor b\right\rfloor+1$ and
$\left\lfloor\frac{\tau_{\alpha,r}}{r}\right\rfloor=0$, we derive
$\frac{\\#A}{r}-1\leq\\#(A\cap S_{\alpha,r})\leq\frac{\\#A}{r}+1$. ∎

See 3

###### Proof.

Let $Q_{d}$ be the set containing the $\min(\\#Q,d)$ smallest primes in $Q$.
Recall that by definition $m(q)\leq d\leq q-1$ for every $q\in Q$. We have,

$W_{m}(Q)^{-1}=\prod_{q\in Q}\frac{q}{q-m(q)}\ \leq\prod_{q\in
Q}\frac{q}{q-d}\ \leq\ \prod_{q\in Q_{d}}\frac{q}{q-d}\cdot\\!\prod_{q\in
Q\setminus Q_{d}}\frac{q}{q-d}\ \leq\ (d+1)^{d}\cdot\\!\prod_{q\in Q\setminus
Q_{d}}\frac{q}{q-d},$

where the last inequality holds because $\frac{x}{x-c}\leq c+1$ for every
$x\geq c+1$ and $c\in\mathbb{Z}_{+}$. Below, let us denote by $p_{i}$ the
$i$-th prime. We further inspect the product $\prod_{q\in Q\setminus
Q_{d}}\frac{q}{q-d}$:

$\displaystyle\prod_{q\in Q\setminus
Q_{d}}\frac{q}{q-d}\leq\prod_{i=d+1}^{\\#Q}\frac{p_{i}}{p_{i}-d}\leq\prod_{i=d+1}^{\\#Q}\frac{i\cdot\ln
i}{i\cdot\ln i-d}$ $\displaystyle\begin{aligned} \text{$p_{i}\geq i\cdot\ln i$
for all $i\in\mathbb{Z}_{+}$,
see~{}\cite[cite]{[\@@bibref{Number}{Rosser39}{}{}]};}\\\
\text{$x\mapsto\frac{x}{x-d}$ decreasing for $x>1$}\end{aligned}$
$\displaystyle\leq\,$
$\displaystyle\exp\left({\sum_{i=d+1}^{\\#Q}\ln\Big{(}\frac{i\cdot\ln
i}{i\cdot\ln
i-d}\Big{)}}\right)=\exp\left({-\sum_{i=d+1}^{\\#Q}\ln\Big{(}1-\frac{d}{i\cdot\ln
i}\Big{)}}\right)$ $\displaystyle\leq\,$
$\displaystyle\exp\left({\sum_{i=d+1}^{\\#Q}\frac{3\cdot d}{i\cdot\ln
i}}\right)\leq\exp\left({\sum_{i=2}^{\\#Q}\frac{3\cdot d}{i\cdot\ln
i}}\right)$ $\displaystyle\begin{aligned} \text{first term from
$\ln\Big{(}1-\frac{1}{x}\Big{)}\geq-\frac{3}{x}$ for all $x\geq\ln 3$;}\\\
\text{for corner case $d=1$ and $i=2$, note $2\ln 2>\ln 3$}\end{aligned}$
$\displaystyle\leq\,$ $\displaystyle\exp\left(\frac{3\cdot d}{2\cdot\ln
2}+{\sum_{i=3}^{\\#Q}\frac{3\cdot d}{i\cdot\ln
i}}\right)\leq\exp\left(\frac{3\cdot d}{2\cdot\ln
2}+\int_{2}^{\\#Q+1}\frac{3\cdot d}{x\ln x}\textup{d}x\right)$
$\displaystyle\begin{aligned} \text{Riemann over-approximation}\\\ \text{note:
$\\#Q+1\geq 2$}\end{aligned}$ $\displaystyle\leq\,$
$\displaystyle\exp\left(\frac{3\cdot d}{2\cdot\ln 2}+3\cdot
d\cdot\big{(}\ln\ln(\\#Q+1)-\ln\ln 2\,\big{)}\right)\leq\exp\left(3\cdot
d\cdot\big{(}2+\ln\ln(\\#Q+1)\big{)}\right).$

We plug this bound on the afore-derived bound for $W_{m}(Q)^{-1}$ to complete
the proof of 3:

$\displaystyle W_{m}(Q)^{-1}$ $\displaystyle\leq\,(d+1)^{d}\exp\left(3\cdot
d\cdot\big{(}2+\ln\ln(\\#Q+1)\big{)}\right)\,\leq\,(d+1)^{d}\cdot e^{6\cdot
d}\ln(\\#Q+1)^{3\cdot d}$ $\displaystyle\leq\,(d+1)^{d}\cdot 2^{9\cdot
d}\ln(\\#Q+1)^{3\cdot d}\,\leq\,(d+1)^{10\cdot d}\ln(\\#Q+1)^{3\cdot d}.\qed$

##  Appendix C Algorithms related to the elimination property

In this appendix we establish Lemma 6 and Lemma 7. Proving these lemmas
require the standard notion of kernel and Hermite normal form of a matrix,
which we now recall for completeness. Consider a matrix
${A\in\mathbb{Z}^{n\times d}}$. The _kernel_ of $A$ is the vector space
$\ker(A)\coloneqq\\{\boldsymbol{v}\in\mathbb{Z}^{d}:A\cdot\boldsymbol{v}=\boldsymbol{0}\\}$.
We represent  _bases_ of $\ker(A)$ as matrices
$K\in\mathbb{Z}^{d\times(d-r)}$, where $r$ is the rank of $A$ and
$\ker(A)=\\{K\cdot\boldsymbol{v}:\boldsymbol{v}\in\mathbb{Z}^{d-r}\\}$. A
matrix $H\in\mathbb{Z}^{n\times d}$ is said to be the _column-style Hermite
normal form_ of $A$ (HNF, in short) if there is a square unimodular matrix
$U\in\mathbb{Z}^{d\times d}$ such that $H=A\cdot U$ and

  1. 1.

$H$ is lower triangular,

  2. 2.

the _pivot_ (i.e., the first non-zero entry in a column, from the top) of a
non-zero column is positive and it is strictly below the pivot of the column
before it, and

  3. 3.

elements to the right of pivots are $0$ and elements to the left are non-
negative and smaller than the pivot.

Recall that $U$ being unimodular means that it is invertible over the
integers.

Given a vector $\boldsymbol{v}$, we write $\boldsymbol{v}[i]$ for the $i$-th
entry of $\boldsymbol{v}$, starting at $i=1$. Similarly, for a matrix $A$, we
write $A[i]$ for its $i$-th row, again starting at $i=1$.

######  Proposition 6 ([19, Section 4.2]).

The HNF $H$ of a matrix $A\in\mathbb{Z}^{n\times d}$ always exits, it is
unique, and $A$ and $H$ generate the same lattice, i.e.,
$\\{A\cdot\boldsymbol{\lambda}:\boldsymbol{\lambda}\in\mathbb{Z}^{d}\\}=\\{H\cdot\boldsymbol{\lambda}:\boldsymbol{\lambda}\in\mathbb{Z}^{d}\\}$.

The following proposition refers to the LLL-based algorithm for the HNF in
[8]. A basis for the integer kernel can be retrieved from the HNF together
with the associated unimodular matrix.

######  Proposition 7 ([24]).

There is a PTIME algorithm computing a basis $K$ of the integer kernel and the
HNF $H$ of an input matrix $A\in\mathbb{Z}^{n\times d}$. The algorithm yields
${{|\mkern-2.0mu|}K{|\mkern-2.0mu|},{|\mkern-2.0mu|}H{|\mkern-2.0mu|}\leq(n\cdot{|\mkern-2.0mu|}A{|\mkern-2.0mu|}+1)^{O(n)}}$.

Note that we can also upper bound the GCDs of the rows of the integer kernel
$K$ in terms of the rank of $A$ by appealing to Proposition 3.

######  Corollary 2.

Consider a basis $K$ of the integer kernel of a matrix
$A\in\mathbb{Z}^{n\times d}$. Let $r\coloneqq\textup{rank}(A)$. For every
$i\in[1,d]$,
${|\mkern-2.0mu|}\gcd(K[i]){|\mkern-2.0mu|}\leq(d+1)\cdot(r\cdot\max(2,{|\mkern-2.0mu|}A{|\mkern-2.0mu|}))^{r}$.

###  C.1 Computing a set spanning the divisibility module

See 6

This lemma follows from the forthcoming Proposition 8 and Proposition 9.

For the whole section, let
$\Phi\coloneqq\bigwedge_{i=1}^{m}f_{i}\mathrel{|}g_{i}$ and $f$ be a primitive
polynomial. As already explained in Section 3, the algorithm Lemma 6 refers to
performs a fix-point computation where, at the $\ell$-th iteration, the values
contained in $\boldsymbol{v}$ characterize a spanning set of a particular
submodule $\textup{M}_{f}^{\ell}(\Phi)$ of $\textup{M}_{f}(\Phi)$. More
precisely, we define
$\textup{M}^{0}_{f}(\Phi)\subseteq\textup{M}^{1}_{f}(\Phi)\subseteq\dots\subseteq\textup{M}^{\ell}_{f}(\Phi)\subseteq\dots$
to be the sequence of sets given by

  1. 1.

$\textup{M}_{f}^{0}(\Phi)\coloneqq\mathbb{Z}f$, and

  2. 2.

for $\ell\in\mathbb{N}$,
$\textup{M}_{f}^{\ell+1}(\Phi)\coloneqq\textup{M}_{f}^{\ell}(\Phi)+\left\\{\textstyle\sum_{j=1}^{m}a_{j}\cdot
g_{j}:\text{ for all }i\in[1,m],\,a_{i}\in\mathbb{Z}\text{ and }a_{i}\cdot
f_{i}\in\textup{M}_{f}^{\ell}(\Phi)\right\\}\\!.$

Let $\ell\in\mathbb{N}$. Note that, by definition,
$\textup{M}_{f}^{\ell}(\Phi)$ is a $\mathbb{Z}$-module and moreover if
$\mathbb{Z}f_{i}\cap\textup{M}_{f}^{\ell}(\Phi)=\\{0\\}$ for some $i\in[1,m]$,
then $a_{i}$ in the definition of $\textup{M}_{f}^{\ell+1}(\Phi)$ equals $0$.
We define the _canonical representation_ of $\textup{M}_{f}^{\ell}(\Phi)$ as
the vector $(v_{1},\dots,v_{m})\in\mathbb{N}^{m}$ such that for every
$i\in[1,m]$,

  * •

if $\ell=0$ then $v_{i}\coloneqq 0$,

  * •

if $\ell\geq 1$ then $v_{i}\coloneqq\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot
f_{i}\in\textup{M}_{f}^{\ell-1}(\Phi)\\}$.

Lemma 16 shows that this vector represents a spanning set of
$\textup{M}_{f}^{\ell}(\Phi)$, but first we need an auxiliary lemma.

######  Lemma 15.

Let $\ell\in\mathbb{N}$. Let $(v_{1},\dots,v_{m})$ and
$(v_{1}^{\prime},\dots,v_{m}^{\prime})$ be the canonical representations of
$\textup{M}_{f}^{\ell}(\Phi)$ and $\textup{M}_{f}^{\ell+1}(\Phi)$,
respectively. For every $i\in[1,m]$, $v_{i}=v_{i}^{\prime}=0$ or
$v_{i}^{\prime}$ divides $v_{i}$ (so, $v_{i}^{\prime}\neq 0$ if $v_{i}\neq
0$).

###### Proof.

Let $i\in[1,m]$. If $v_{i}=0$ then either $v_{i}^{\prime}$ is $0$ or it
divides $v_{i}$, hence the statement is trivially satisfied for that
particular $i$. Suppose that $v_{i}\neq 0$. By definition of canonical
representation, $\ell\geq 1$ and $v_{i}\cdot f_{i}\in M^{\ell-1}_{f}(\Phi)$.
By definition of $\textup{M}_{f}^{\ell}(\Phi)$, we conclude that $v_{i}\cdot
f_{i}\in M^{\ell}_{f}(\Phi)$. By definition of canonical representation
$v_{i}^{\prime}=\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot
f_{i}\in\textup{M}_{f}^{\ell}(\Phi)\\}$, and therefore $v_{i}^{\prime}$
divides $v_{i}$. ∎

######  Lemma 16.

Let $\ell\in\mathbb{N}$ and let $(v_{1},\dots,v_{m})\in\mathbb{N}^{m}$ be the
canonical representation of $\textup{M}_{f}^{\ell}(\Phi)$. Then, the set of
linear polynomials $\\{f,\,v_{1}\cdot g_{1},\,\dots,\,v_{m}\cdot g_{m}\\}$
spans $M^{\ell}_{f}(\Phi)$.

###### Proof.

The statement follows by induction on $\ell\in\mathbb{N}$.

base case $\ell=0$.

From $\textup{M}_{f}^{0}(\Phi)=\mathbb{Z}f$ we have
$(v_{1},\dots,v_{m})=(0,\dots,0)$ and $\\{f\\}$ spans $M^{0}_{f}(\Phi)$.

induction step $\ell\geq 1$.

From the induction hypothesis, ${\\{f,\,v_{1}^{*}\cdot
g_{1},\,\dots,\,v_{m}^{*}\cdot g_{m}\\}}$ spans $M^{\ell-1}_{f}(\Phi)$; with
$(v_{1}^{*},\dots,v_{m}^{*})$ being the canonical representation of
$M^{\ell-1}_{f}(\Phi)$. We consider the two inclusions of the equivalence
$\mathbb{Z}f+\mathbb{Z}(v_{1}\cdot g_{1})+\dots+\mathbb{Z}(v_{m}\cdot
g_{m})=M^{\ell}_{f}(\Phi)$.

$(\subseteq):$ This direction follows directly by definition of
$M^{\ell}_{f}(\Phi)$.

$(\supseteq):$ Let $h\in\textup{M}_{f}^{\ell}(\Phi)$. By definition,
$h=h_{1}+h_{2}$ where ${h_{1}\in\mathbb{Z}f+\mathbb{Z}(v_{1}^{*}\cdot
g_{1})+\dots+\mathbb{Z}(v_{m}^{*}\cdot g_{m})}$ and
$h_{2}=\sum_{i=1}^{m}a_{i}\cdot g_{i}\in\textup{M}_{f}^{\ell}(\Phi)$
satisfying ${a_{i}\cdot f_{i}\in\textup{M}_{f}^{\ell-1}(\Phi)}$ for every
$i\in[1,m]$. By Lemma 15 $\mathbb{Z}(v_{i}^{*}\cdot
g_{i})\subseteq\mathbb{Z}(v_{i}\cdot g_{i})$ and therefore
$h_{1}\in\mathbb{Z}f+\mathbb{Z}(v_{1}\cdot g_{1})+\dots+\mathbb{Z}(v_{m}\cdot
g_{m})$. By definition $v_{i}=\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot
f_{i}\in\textup{M}_{f}^{\ell-1}(\Phi)\\}$ and thus $v_{i}\mathrel{|}a_{i}$.
So, $h\in\mathbb{Z}f+\mathbb{Z}(v_{1}\cdot g_{1})+\dots+\mathbb{Z}(v_{m}\cdot
g_{m})$. ∎

######  Lemma 17.

(A) For every $\ell\in\mathbb{N}$,
$\textup{M}_{f}^{\ell}\subseteq\textup{M}_{f}^{\ell+1}\subseteq\textup{M}_{f}(\Phi)$.

(B) There is $\ell\in\mathbb{N}$ such that
$\textup{M}_{f}^{\ell}(\Phi)=\textup{M}_{f}^{\ell+1}(\Phi)$.

(C) For every $\ell\in\mathbb{N}$, if
$\textup{M}_{f}^{\ell}(\Phi)=\textup{M}_{f}^{\ell+1}(\Phi)$ then
$\textup{M}_{f}^{\ell}(\Phi)=\textup{M}_{f}(\Phi)$.

###### Proof.

Proof of (17): By definition,
$\textup{M}_{f}^{\ell}\subseteq\textup{M}_{f}^{\ell+1}$. An induction on
$\ell\in\mathbb{N}$ shows $M^{\ell}_{f}(\Phi)\subseteq\textup{M}_{f}(\Phi)$:

base case $\ell=0$:

By definition of $\textup{M}_{f}^{\ell}(\Phi)$ and of divisibility module,
$M^{0}_{f}(\Phi)=\mathbb{Z}f\subseteq\textup{M}_{f}(\Phi)$.

induction case $\ell\geq 1$:

From the induction hypothesis,
$M^{\ell-1}_{f}(\Phi)\subseteq\textup{M}_{f}(\Phi)$. By definition,
$M^{\ell}_{f}(\Phi)$ is defined from $M^{\ell-1}_{f}(\Phi)$ by taking linear
combinations of elements in $M^{\ell-1}_{f}(\Phi)$ together with elements
$b\cdot h$ such that $b\cdot g\in M^{\ell-1}_{f}(\Phi)$ and $g\mathrel{|}h$ is
a divisibility of $\Phi$. From the definition of divisibility module,
$\textup{M}_{f}(\Phi)$ is closed under such combinations, since for every
$b\cdot g\in\textup{M}_{f}(\Phi)$ and $g\mathrel{|}h$ divisibility of $\Phi$,
$b\cdot h\in\textup{M}_{f}(\Phi)$ (see Property iii in the def. of
divisibility module). From $M^{\ell-1}_{f}(\Phi)\subseteq\textup{M}_{f}(\Phi)$
we then conclude that $M^{\ell}_{f}(\Phi)\subseteq\textup{M}_{f}(\Phi)$.

Proof of (17): This statement follows from Lemma 15. Indeed, for a given
$\ell\in\mathbb{N}$, consider the canonical representations
$(v_{1},\dots,v_{m})$ and $(v_{1}^{\prime},\dots,v_{m}^{\prime})$ of
$\textup{M}_{f}^{\ell}(\Phi)$ and $\textup{M}_{f}^{\ell+1}(\Phi)$,
respectively. By Lemma 15, if
$\textup{M}_{f}^{\ell}(\Phi)\neq\textup{M}_{f}^{\ell+1}(\Phi)$ then one of the
following holds:

  1. 1.

there is $i\in[1,m]$ such that $v_{i}=0$ and $v_{i}^{\prime}\neq 0$, or

  2. 2.

there is $i\in[1,m]$ such that $v_{i}\neq 0$, $v_{i}^{\prime}\neq v_{i}$ and
$v_{i}^{\prime}$ divides $v_{i}$.

Again from Lemma 15, for every $j\in[1,m]$, if $v_{j}\neq 0$ then
$v_{j}^{\prime}$ divides $v_{j}$. This implies that both Items (1) and (2)
cannot occur infinitely often, and therefore
$\textup{M}_{f}^{r}(\Phi)=\textup{M}_{f}^{r+1}(\Phi)$ for some
$r\in\mathbb{N}$.
Proof of (17): From Part (17),
$\textup{M}_{f}^{\ell}(\Phi)\subseteq\textup{M}_{f}(\Phi)$. We show that
$\textup{M}_{f}^{\ell}(\Phi)$ satisfies the Properties i–iii of divisibility
modules. Then, $\textup{M}_{f}(\Phi)\subseteq\textup{M}_{f}^{\ell}(\Phi)$
follows from the minimality condition required by these modules. Properties i
and ii are trivially satisfied. To establish Property iii, consider $b\cdot
g\in\textup{M}_{f}^{\ell}(\Phi)$ and a divisibility $g\mathrel{|}h$ of $\Phi$.
By definition $b\cdot h\in\textup{M}_{f}^{\ell+1}(\Phi)$, and from
$\textup{M}_{f}^{\ell}=\textup{M}_{f}^{\ell+1}(\Phi)$ we get $b\cdot
h\in\textup{M}_{f}^{\ell}(\Phi)$. Therefore, $\textup{M}_{f}^{\ell}(\Phi)$
satisfies Property iii. ∎

In view of Lemmas 16 and 17, the algorithm required by Lemma 6 presents
itself: it suffices to iteratively compute canonical representations of every
$\textup{M}_{f}^{\ell}(\Phi)$ until reaching a fix-point. Algorithm 4 performs
this computation.

Algorithm 4 Computes a set spanning a divisibility module

1:A system of divisibility constraints
$\Phi(\boldsymbol{x})=\bigwedge_{i=1}^{m}f_{i}(\boldsymbol{x})\mathrel{|}g_{i}(\boldsymbol{x})$
and a primitive polynomial $f$.

2:A tuple $(c_{1},\dots,c_{m})\in\mathbb{N}^{m}$ such that $\\{f,\,c_{1}\cdot
g_{1},\,\dots,\,c_{m}\cdot g_{m}\\}$ spans $\textup{M}_{f}(\Phi)$.

3:$\boldsymbol{v}\coloneqq(0,\dots,0)\in\mathbb{N}^{m}$

4:while true do

5: $\boldsymbol{u}\coloneqq\boldsymbol{v}$

6: for $i$ in $[1,m]$ do

7: $F_{i}\coloneqq\\{-f_{i},\,f,\,\boldsymbol{u}[1]\cdot
g_{1},\,\dots,\,\boldsymbol{u}[m]\cdot g_{m}\\}$

8: $K_{i}\coloneqq$ basis of the integer kernel of the matrix representing
$F_{i}$

9: $\boldsymbol{v}[i]\leftarrow\gcd(\text{row of $K_{i}$ corresponding to
$-f_{i}$})$

10: if $\boldsymbol{v}=\boldsymbol{u}$ then return $\boldsymbol{v}$

In a nutshell, during the $\ell$-th iteration ($\ell\geq 1$) of the while loop
of line 4, the variable $\boldsymbol{u}$ contains the canonical representation
of $\textup{M}_{f}^{\ell-1}(\Phi)$, and the algorithm updates the vector
$\boldsymbol{v}$ with the canonical representation of
$\textup{M}_{f}^{\ell}(\Phi)$. To update the value $\boldsymbol{v}[i]$
associated to $g_{i}$ the algorithm needs to compute
$\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot
f_{i}\in\textup{M}_{f}^{\ell-1}(\Phi)\\}$ (line 9). This is done by finding a
finite representation for all the scalars $\lambda$, which is given by those
entries corresponding to $-f_{i}$ in a basis of the integer kernel of the
matrix for the set $F_{i}$ defined in line 7. As explained in Section 3.1, a
set of polynomials $F\coloneqq\\{h_{1},\dots,h_{\ell}\\}$ in variables
$x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$ (where $\mathbin{\prec}$ is an
arbitrary order) can be represented as the matrix
$A\in\mathbb{Z}^{(d+1)\times\ell}$ in which each column
$(a_{d},\dots,a_{1},c)$ contains the coefficients and the constant of a
distinct element $h$ of $F$, with $a_{i}$ being the coefficient of $x_{i}$ for
$i\in[1,d]$, and $c$ being the constant of $h$. This matrix is unique up-to
permutation of columns.

It might not be clear for the moment whether Algorithm 4 runs in PTIME: in
each iteration, the integer kernel computation done in line 8 might a priori
increase the bit length of the entries in the canonical representation by a
polynomial factor, yielding entries of exponential bit length after
polynomially many iterations – an effect similar to naïve implementations of
Gaussian elimination or kernel computations via suboptimal algorithms for the
Hermite normal form of a matrix. We show later that our worries are
unjustified, as the GCD computed in line 9 prevents this blow-up. For the
moment, let us formally argue on the correctness of Algorithm 4.

######  Proposition 8.

Algorithm 4 respects its specification.

###### Proof.

We write $\boldsymbol{u}_{\ell}$ for the value that the tuple $\boldsymbol{u}$
declared in line 5 of Algorithm 4 takes during the $(\ell+1)$-th iterations of
the while loop of line 4, with $\ell\in\mathbb{N}$ and assuming that the while
loop is iterated at least $\ell+1$ times. We show the following claim:

######  Claim 9.

For every $\ell\in\mathbb{N}$, the tuple $\boldsymbol{u}_{\ell}$ is the
canonical representation of $\textup{M}_{f}^{\ell}(\Phi)$.

Since Algorithm 4 terminates when $\boldsymbol{u}_{\ell-1}$ is found to be
equal to $\boldsymbol{u}_{\ell}$ for some $\ell\geq 1$, its correctness
follows directly from Lemma 16 and Lemma 17. The proof of this claim is by
induction on $\ell$.

base case.

We have $\boldsymbol{u}_{0}=(0,\dots,0)\in\mathbb{N}^{m}$, which is the
canonical representation of $\textup{M}_{f}^{0}(\Phi)$.

induction step.

By induction hypothesis, let us assume that
$\boldsymbol{u}_{\ell}=(v_{1},\dots,v_{m})$ is the canonical representation of
$\textup{M}_{f}^{\ell}(\Phi)$. We show that when exiting the for loop of line
6, for every $i\in[1,m]$, $\boldsymbol{v}[i]$ equals
$v_{i}^{\prime}\coloneqq\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot
f_{i}\in\textup{M}_{f}^{\ell}(\Phi)\\}$. Thanks to the declaration of line 5,
this implies that $\boldsymbol{u}_{\ell+1}$ is the canonical representation of
$\textup{M}_{f}^{\ell+1}(\Phi)$. Since
$\boldsymbol{u}_{\ell}=(v_{1},\dots,v_{m})$ is the canonical representation of
$\textup{M}_{f}^{\ell}(\Phi)$, by Lemma 16 we have
$\textup{M}_{f}^{\ell}(\Phi)=\mathbb{Z}f+\mathbb{Z}(v_{1}\cdot
g_{1})+\dots+\mathbb{Z}(v_{m}\cdot g_{m})$. Therefore,
$v_{i}^{\prime}=\gcd\\{\lambda\in\mathbb{N}:\lambda\cdot f_{i}=\mu_{0}\cdot
f+\textstyle\sum_{i=1}^{m}\mu_{i}\cdot(v_{i}\cdot g_{i})\text{ for some
}\mu_{0},\dots,\mu_{m}\in\mathbb{Z}\\}$. The set of tuples
$(\lambda,\mu_{0},\dots,\mu_{m})\in\mathbb{Z}^{m+2}$ such that $\lambda\cdot
f_{i}=\mu_{0}\cdot f+\textstyle\sum_{i=1}^{m}\mu_{i}\cdot(v_{i}\cdot g_{i})$
corresponds to the solutions to the system of equations
$A\cdot(\lambda,\mu_{0},\dots,\mu_{m})=\boldsymbol{0}$ over the integers,
where $A$ is the matrix representing the set $\\{-f_{i},\,f,\,v_{i}\cdot
g_{1},\,\dots,\,\boldsymbol{v}_{m}\cdot g_{m}\\}$, i.e., $F_{i}$ in line 7.
This set corresponds to $\ker(A)$, and so can be finitely represented with an
integer kernel basis, i.e., $K_{i}$ in line 8. Computing $v_{i}^{\prime}$ only
requires to compute the GCD of the row of $K_{i}$ corresponding to the
variable $\lambda$ of $-f_{i}$. This is exactly how $\boldsymbol{v}[i]$ is
defined in line 9. ∎

We move to the runtime analysis of Algorithm 4. We need the following lemma
studying the growth of the GCDs of the rows of bases $K$ of $\ker(A)$ when
columns of $A$ are scaled by positive integers. In the lemma below,
$\textup{diag}(c_{1},\dots,c_{d})$ stands for the $d\times d$ diagonal matrix
having $c_{1},\dots,c_{d}$ in the main diagonal.

######  Lemma 18.

Consider a matrix $A\in\mathbb{Z}^{n\times d}$ of rank $r$, integers
$c_{1},\dots,c_{d}>0$, and let $K,K^{\prime}\in\mathbb{Z}^{d\times(d-r)}$ be
bases of the integer kernels of $A$ and $A^{\prime}\coloneqq
A\cdot\textup{diag}(c_{1},\dots,c_{d})$, respectively. For every $i\in[1,d]$,

  1. 1.

if $\gcd(K[i])=0$ then $\gcd(K^{\prime}[i])=0$, and

  2. 2.

if $\gcd(K[i])>0$ then $\gcd(K^{\prime}[i])\neq 0$ and $\gcd(K^{\prime}[i])$
divides $\textup{lcm}(c_{1},\dots,c_{d})\cdot\gcd(K[i])$.

###### Proof.

Note that $A^{\prime}$ is the matrix obtained from $A$ by scaling the $j$-th
column of $A$ by $c_{j}$ ($j\in[1,d]$). Let $i\in[1,d]$ and
$(M,J)\in\\{(A,K),(A^{\prime},K^{\prime})\\}$. By definition of kernel,
${\\{J\cdot\boldsymbol{\lambda}:\boldsymbol{\lambda}\in\mathbb{Z}^{m}\\}}=\\{\boldsymbol{x}\in\mathbb{Z}^{d}:M\cdot\boldsymbol{x}=\boldsymbol{0}\\}$.
This fact has three direct consequences:

  1. (A)

if $\gcd(J[i])=0$, then no vector
$\boldsymbol{x}=(x_{1},\dots,x_{d})\in\mathbb{Z}^{d}$ satisfies both
$x_{i}\neq 0$ and $M\cdot\boldsymbol{x}=0$,

  2. (B)

if $\gcd(J[i])>0$, then there is
$\boldsymbol{x}=(x_{1},\dots,x_{d})\in\mathbb{Z}^{d}$ such that
$x_{i}=\gcd(J[i])$ and $M\cdot\boldsymbol{x}=0$,

  3. (C)

if $\gcd(J[i])>0$, then for every
$\boldsymbol{x}=(x_{1},\dots,x_{d})\in\mathbb{Z}^{d}$ satisfying
$M\cdot\boldsymbol{x}=0$ we have $\gcd(J[i])\mathrel{|}x_{i}$.

Items 1 and 2 in the statement of the lemma are derived from these three
properties.
Proof of (1): By contrapositive, assume that $\gcd(K^{\prime}[i])\neq 0$.
Hence, $\gcd(K^{\prime}[i])>0$ and by Item B there is
$\boldsymbol{x}=(x_{1},\dots,x_{d})\in\mathbb{Z}^{d}$ such that
$x_{i}=\gcd(K^{\prime}[i])$ and
$A^{\prime}\cdot\boldsymbol{x}=\boldsymbol{0}$. Let
$\boldsymbol{y}\coloneqq(c_{1}\cdot x_{1},\dots,c_{d}\cdot x_{d})$. We have
$A\cdot\boldsymbol{y}=A\cdot(\textup{diag}(c_{1},\dots,c_{d})\cdot\boldsymbol{x})=(A\cdot\textup{diag}(c_{1},\dots,c_{d}))\cdot\boldsymbol{x}=A^{\prime}\cdot\boldsymbol{x}=\boldsymbol{0}$.
Since $c_{i}>0$ we have $c_{i}\cdot x_{i}\neq 0$, which together with
$A\cdot\boldsymbol{y}=\boldsymbol{0}$ implies $\gcd(K[i])\neq 0$ by Item A.
Proof of (2): Suppose $\gcd(K[i])>0$. By Item B, there is
$\boldsymbol{x}=(x_{1},\dots,x_{d})\in\mathbb{Z}^{d}$ with
$A\cdot\boldsymbol{x}=\boldsymbol{0}$ and $x_{i}=\gcd(K[i])$. Define
$C\coloneqq\textup{lcm}(c_{1},\dots,c_{d})$ and
$\boldsymbol{y}\coloneqq(\frac{C}{c_{1}}\cdot x_{1},\dots,\frac{C}{c_{d}}\cdot
x_{d})$. Note that $\boldsymbol{y}\in\mathbb{Z}^{d}$ is well-defined, since
$c_{1},\dots,c_{d}>0$. Moreover, $\frac{C}{c_{i}}\cdot
x_{i}=\frac{C}{c_{i}}\cdot\gcd(K[i])>0$. We have,

$\displaystyle A^{\prime}\cdot\boldsymbol{y}$
$\displaystyle\textstyle=A^{\prime}\cdot(\textup{diag}(\frac{C}{c_{1}},\dots,\frac{C}{c_{d}})\cdot\boldsymbol{x})\
=\
(A\cdot\textup{diag}(c_{1},\dots,c_{d}))\cdot(\textup{diag}(\frac{C}{c_{1}},\dots,\frac{C}{c_{d}})\cdot\boldsymbol{x})$
$\displaystyle\textstyle=A\cdot(\textup{diag}(c_{1},\dots,c_{d})\cdot\textup{diag}(\frac{C}{c_{1}},\dots,\frac{C}{c_{d}}))\cdot\boldsymbol{x}\
=\ C\cdot A\cdot\boldsymbol{x}\ =\ \boldsymbol{0}.$

Then, by Item A, $\gcd(K^{\prime}[i])>0$, which in turn implies that
$\gcd(K^{\prime}[i])\mathrel{|}\frac{C}{c_{i}}\cdot x_{i}$, directly from Item
C. Therefore, $\gcd(K^{\prime}[i])$ divides
$\textup{lcm}(c_{1},\dots,c_{d})\cdot\gcd(K[i])$. ∎

We are now ready to discuss the runtime of Algorithm 4.

######  Proposition 9.

Algorithm 4 runs in PTIME, and on an input $(\Phi,f)$ such that
$\Phi=\bigwedge_{i=1}^{m}f_{i}\mathrel{|}g_{i}$ it returns a vector
$\boldsymbol{v}$ satisfying
${|\mkern-2.0mu|}\boldsymbol{v}{|\mkern-2.0mu|}\leq((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)^{3}}$.

###### Proof.

As done in the proof of Proposition 8, let
$\boldsymbol{u}_{\ell}\in\mathbb{Z}^{m}$ be the value that the tuple
$\boldsymbol{u}$ declared in line 5 takes during the $(\ell+1)$-th iteration
of the while of line 4, with $\ell\in\mathbb{N}$ and assuming that the while
loop is iterated at least $\ell+1$ times. Similarly, given $j\in[1,m]$, let
$F_{\ell,j}$ and $K_{\ell,j}$ be the set of polynomial and matrix declared in
lines 7 and 8, respectively, during the $(\ell+1)$-th iteration of the while
loop and at the end of the iteration of the for loop of line 7 where the index
variable $i$ takes value $j$. Lastly, following the code in line 9, we define
$v_{\ell,j}\coloneqq\gcd(\text{row of $K_{\ell,j}$ corresponding to
$-f_{j}$})$. A few preliminary remarks that follow directly form the
definitions above:

For the runtime of the algorithm, first consider the case where
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}f_{j}=\\{0\\}$ for every $j\in[1,m]$, which
implies $\textup{M}_{f}(\Phi)=\mathbb{Z}f$, by definition of divisibility
module. Focus on the first execution of the body of the while loop. Since
$\boldsymbol{u}_{0}=(0,\dots,0)$, for every $j\in[1,m]$,
$F_{0,j}=\\{-f_{j},\,f\\}$. Since
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}f_{j}=\\{0\\}$, the row of $K_{0,j}$
corresponding to $-f_{j}$ contains only zeros. This implies
$\boldsymbol{v}=(0,\dots,0)=\boldsymbol{u}_{0}$ in line 10, and Algorithm 4
returns $(0,\dots,0)$ after a single iteration of the while.

Consider now the case where
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}f_{j}\neq\emptyset$ for some $j\in[1,m]$.
Note that this implies $f_{j}=a\cdot f$ for some
$a\in\mathbb{Z}\setminus\\{0\\}$ and $j\in[1,m]$, hence $\langle
f\rangle\leq\mathrm{poly}(\langle\Phi\rangle)$. This allows us to bound the
size of the output of Algorithm 4 in terms of $\Phi$, hiding factors that
depend on $f$ (as done in the statement of the proposition). A few auxiliary
definitions are handy ($\ell\in\mathbb{N}$ and $j\in[1,m]$):

  * •

We associate to $\boldsymbol{u}_{\ell}$ the vector
$\widehat{\boldsymbol{u}}_{\ell}\in\\{0,1\\}^{m}$ given by
$\widehat{\boldsymbol{u}}_{\ell}[i]=1$ iff $\boldsymbol{u}_{\ell}[i]\neq 0$,
for every $i\in[1,m]$.

  * •

We associate to $F_{\ell,j}$ the set
$\widehat{F}_{\ell,j}\coloneqq\\{-f_{j},\,f,\,\widehat{\boldsymbol{u}}_{\ell}[1]\cdot
g_{1},\,\dots,\,\widehat{\boldsymbol{u}}_{\ell}[m]\cdot g_{m}\\}$.

  * •

We associate to $K_{\ell,j}$ a basis $\widehat{K}_{\ell,j}$ for the integer
kernel of the matrix representing $\widehat{F}_{\ell,j}$.

  * •

We associate to $v_{\ell,j}$ the integer
$\widehat{v}_{\ell,j}\coloneqq\gcd(\text{row of $\widehat{K}_{\ell,j}$
corresponding to $-f_{j}$})$.

In a nutshell, $\widehat{\boldsymbol{u}}_{\ell}$ “forgets” the magnitude of
the integers stored in $\boldsymbol{u}_{\ell}$, keeping only whether their
value was $0$ or not. The other objects defined above reflect this change at
the level of matrices, kernels and GCDs. Up to permutation of columns, the
matrix representing $F_{\ell,j}$ can be obtained by multiplying the matrix of
$\widehat{F}_{\ell,j}$ by a diagonal matrix having in the main diagonal (a
permutation of)
$(1,1,\boldsymbol{u}_{\ell}[1],\dots,\boldsymbol{u}_{\ell}[m])$. From the
definition of $\widehat{K}_{\ell,j}$ and by Lemma 18, we conclude that

if $\widehat{v}_{\ell,j}=0$ then $v_{\ell,j}=0$, and if
$\widehat{v}_{\ell,j}\neq 0$ then $v_{\ell,j}\neq 0$ and $v_{\ell,j}$ divides
$\textup{lcm}(\boldsymbol{u}_{\ell})\cdot\widehat{v}_{\ell,j}$. ($\dagger$)

Recall that the matrix representing $\widehat{F}_{\ell,j}$ has $d+1$ rows and
$m+2$ columns. Since
${|\mkern-2.0mu|}\widehat{F}_{\ell,j}{|\mkern-2.0mu|}\leq{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}$
for every $\ell\in\mathbb{N}$ and $j\in[1,m]$, by Corollary 2 there an integer
$N\in[2,\,{((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)}}]$
such that $N$ is greater than $\widehat{v}_{\ell,j}$, for every
$\ell\in\mathbb{N}$ and $j\in[1,m]$. We use ($\dagger$ ‣ C.1) above to bound
the number of iterations and magnitude of the entries of
$\boldsymbol{u}_{\ell}$ during the procedure. We show that

  1. 1.

$\max_{\ell\in\mathbb{N}}(\textup{lcm}(\boldsymbol{u}_{\ell}))=\max_{\ell=0}^{m}(\textup{lcm}(\boldsymbol{u}_{\ell}))\leq
N^{m^{3}}$ and for every $j\in[1,m]$, $\boldsymbol{u}_{m}[j]\leq N^{m^{2}}$,
and

  2. 2.

the while loop of line 4 is iterated at most $m^{3}\cdot\log_{2}(N)+m$ many
times.

In Item (1) above we slightly abused our notation, as $\boldsymbol{u}_{\ell}$
is undefined for $\ell\in\mathbb{N}$ greater or equal than the number of
iterations of the while loop performed by the algorithm. In these cases, we
postulate $\textup{lcm}(\boldsymbol{u}_{\ell})=0$ in order to make the
equivalence in Item (1) well-defined. From the bound
$N\leq((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)}$, Items (1)
and (2) imply that Algorithm 4 runs in PTIME and outputs a vector
$\boldsymbol{v}$ with
${|\mkern-2.0mu|}\boldsymbol{v}{|\mkern-2.0mu|}\leq((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)^{3}}$;
proving the proposition.
Proof of (1): Informally, Item (1) states that $\textup{lcm}(\boldsymbol{u})$
is always bounded by $N^{m^{2}}$, and that $\textup{lcm}(\boldsymbol{u})$
achieves its maximum at most after the first $m$ iterations of the while loop.
We start by proving that
${\max_{\ell=0}^{m}(\textup{lcm}(\boldsymbol{u}_{\ell}))\leq N^{m^{3}}}$ and
that for every $j\in[1,m]$, $\boldsymbol{u}_{m}[j]\leq N^{m^{2}}$ This is done
by induction on $\ell\in[1,m]$, by showing that (whenever defined)
$\boldsymbol{u}_{\ell}$ is such that, for every $j\in[1,m]$, if
${\boldsymbol{u}_{\ell}[j]\neq 0}$ then ${\widehat{v}_{\ell-1,j}\neq 0}$ and
$\boldsymbol{u}_{\ell}[j]$ divides
$\big{(}\widehat{v}_{\ell-1,j}\cdot\prod_{i=0}^{\ell-2}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m})\big{)}$.
Note that then $\boldsymbol{u}_{\ell}[j]\leq N^{m(\ell-1)+1}$, since $N$ is an
upper bound on every $\widehat{v}_{\ell,j}$, and thus for $\ell=m$ we get
$\boldsymbol{u}_{m}[j]\leq N^{m^{2}}$ and
$\textup{lcm}(\boldsymbol{u}_{m})\leq N^{m^{3}}$, as required. Below, let
$\boldsymbol{u}_{\ell}=(c_{1},\dots,c_{m})$. Note that, from line 9 of the
algorithm, if $\ell\geq 1$, then $c_{j}=v_{\ell-1,j}$ for every $j\in[1,m]$.

base case $\ell=1$.

From $\boldsymbol{u}_{0}=(0,\dots,0)$ we have
$F_{0,j}=\widehat{F}_{0,j}=\\{-f_{j},f\\}$ for every $j\in[1,m]$. This implies
$\widehat{v}_{0,j}=v_{0,j}$. From $c_{j}=v_{0,j}$, we conclude that
$c_{j}=\widehat{v}_{0,j}$, completing the base case.

induction step $\ell\geq 2$.

Let $j\in[1,m]$ such that $c_{j}\neq 0$. From ($\dagger$ ‣ C.1) and
$c_{j}=v_{\ell-1,j}$, we get $\widehat{v}_{\ell-1,j}\neq 0$ and
$c_{j}\mathrel{|}(\textup{lcm}(\boldsymbol{u}_{\ell-1})\cdot\widehat{v}_{\ell-1,j})$.
Let $\boldsymbol{u}_{\ell-1}=(c_{1}^{*},\dots,c_{m}^{*})$. From the induction
hypothesis, for every ${k\in[1,m]}$, if $c_{k}^{*}\neq 0$ then
$\widehat{v}_{\ell-2,k}\neq 0$ and
$c_{k}^{*}\mathrel{|}\big{(}\widehat{v}_{\ell-2,k}\cdot\prod_{i=0}^{\ell-3}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m})\big{)}$.
Therefore,

$\textup{lcm}(\boldsymbol{u}_{\ell-1})\ \mathrel{|}\
\textup{lcm}\big{(}(\widehat{v}_{\ell-2,1}\cdot\prod_{i=0}^{\ell-3}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m})),\dots,(\widehat{v}_{\ell-2,m}\cdot\prod_{i=0}^{\ell-3}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m}))\big{)}.$

From the equivalence $\textup{lcm}(a\cdot b,c\cdot b)=\textup{lcm}(a,c)\cdot
b$, the right-hand side of the divisibility above equals
$\prod_{i=0}^{\ell-2}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m})$.
Then, the fact that $c_{j}$ divides
$\big{(}\widehat{v}_{\ell-1,j}\cdot\prod_{i=0}^{\ell-2}\textup{lcm}(\widehat{v}_{i,1},\dots,\widehat{v}_{i,m})\big{)}$
follows directly from
$c_{j}\mathrel{|}(\textup{lcm}(\boldsymbol{u}_{\ell-1})\cdot\widehat{v}_{\ell-1,j})$.

To complete the proof of (1), we now show that
$\max_{\ell\in\mathbb{N}}(\textup{lcm}(\boldsymbol{u}_{\ell}))=\max_{\ell=0}^{m}(\textup{lcm}(\boldsymbol{u}_{\ell}))$.
Directly from 9 in the proof of Proposition 8, we have that for every
$\ell\geq 1$, the vector $\boldsymbol{u}_{\ell}$ is the canonical
representation of $\textup{M}_{f}^{\ell}(\Phi)$. We have,

  1. (A)

for every $j\in[1,m]$, if $\boldsymbol{u}_{\ell}[j]\neq 0$ then
$\boldsymbol{u}_{\ell+1}[j]$ divides $\boldsymbol{u}_{\ell}[j]$ (assuming both
$\boldsymbol{u}_{\ell}$ and $\boldsymbol{u}_{\ell+1}$ defined).

This follows directly from Lemma 15.

  2. (B)

If $\boldsymbol{u}_{\ell}$, $\boldsymbol{u}_{\ell+1}$ and
$\boldsymbol{u}_{\ell+2}$ are defined, and $\boldsymbol{u}_{\ell}$ and
$\boldsymbol{u}_{\ell+1}$ have the same zero entries, then also
$\boldsymbol{u}_{\ell}$ and $\boldsymbol{u}_{\ell+2}$ have the same zero
entries.

Indeed, in this case
$\widehat{\boldsymbol{u}}_{\ell}=\widehat{\boldsymbol{u}}_{\ell+1}$ which
implies $\widehat{v}_{\ell,j}=\widehat{v}_{\ell+1,j}$ for every $j\in[1,m]$.
Now, if $\boldsymbol{u}_{\ell+2}[j]\neq 0$ then $v_{\ell+1,j}\neq 0$ and so
$\widehat{v}_{\ell+1,j}\neq 0$ by ($\dagger$ ‣ C.1). Then
$\widehat{v}_{\ell,j}\neq 0$, and again by ($\dagger$ ‣ C.1) we get
$v_{\ell,j}\neq 0$. If instead $\boldsymbol{u}_{\ell+2}[j]=0$, then
$\boldsymbol{u}_{\ell}[j]=0$ follows from Lemma 15.

Since $\boldsymbol{u}$ is a tuple with $m$ entries, Item (B) above ensures
that every $\boldsymbol{u}_{\ell}$ and $\boldsymbol{u}_{r}$ with $\ell,r\geq
m$ share the same zero entries. Item (A) states instead that every non-zero
entry of $\boldsymbol{u}_{\ell}$ upper bounds the corresponding entry of
$\boldsymbol{u}_{\ell+r}$, for every $r\in\mathbb{N}$, and that this latter
entry is always non-zero. Together, Items (A) and (B) imply that
$\max_{\ell\in\mathbb{N}}(\textup{lcm}(\boldsymbol{u}_{\ell}))=\max_{\ell=0}^{m}(\textup{lcm}(\boldsymbol{u}_{\ell}))$.
Proof of (2): Assume that the while loop iterates at least $m+1$ times
(otherwise (2) is trivially satisfied). From (2), the vector
$\boldsymbol{u}_{m}$ such that $\boldsymbol{u}_{m}[j]\leq N^{m^{2}}$ for every
$j\in[1,m]$. As we have just discussed above, by Item (B), every subsequent
$\boldsymbol{u}_{m+r}$ with $r\in\mathbb{N}$ has the same zero entries as
$\boldsymbol{u}_{m}$. Whenever $\boldsymbol{u}_{m+r}$ and
$\boldsymbol{u}_{m+r+1}$ are both defined (meaning in particular that
$\boldsymbol{u}_{m+r}\neq\boldsymbol{u}_{m+r+1}$), there must be $j\in[1,m]$
such that $\boldsymbol{u}_{m+r}[j]\neq\boldsymbol{u}_{m+r+1}[j]$, and moreover
by Item (A), $\boldsymbol{u}_{m+r+1}[i]$ divides $\boldsymbol{u}_{m+r}[i]$ for
every $i\in[1,m]$, which in particular implies that
$\boldsymbol{u}_{m+r+1}[j]\leq\frac{\boldsymbol{u}_{m+r}[j]}{2}$. Therefore,
the product of all non-zero entries of $\boldsymbol{u}$ (at least) halves at
each iteration of the while loop after the $m$-th one. By (1), for every
$j\in[1,m]$ we have $\boldsymbol{u}_{m}[j]\leq N^{m^{2}}$, so the product of
all non-zero entries in $\boldsymbol{u}_{m}$ is bounded by $N^{m^{3}}$. We
conclude that the number of iterations of the while loop after the $m$-th one
is bounded by $\log_{2}(N^{m^{3}})=m^{3}\cdot\log_{2}(N)$; i.e.,
$m^{3}\cdot\log_{2}(N)+m$ many iterations overall. ∎

###  C.2 Closing a system of divisibility constraints under the elimination
property

See 7

###### Proof.

The algorithm is simple to state:

1: $F\coloneqq\\{f\text{ primitive }:\text{$a\cdot f$ is in the left-hand side
of a divisibility of $\Phi$, for some $a\in\mathbb{Z}\setminus\\{0\\}$}\\}$

2:for $f\in F$ do

3: $\boldsymbol{v}\coloneqq(c_{1},\dots,c_{m})\in\mathbb{Z}^{m}$ s.t.
$\\{f,c_{1}\cdot g_{1},\dots,c_{m}\cdot g_{m}\\}$ spans $\textup{M}_{f}(\Phi)$
$\triangleright$ Lemma 6

4: $H$ $\coloneqq$ HNF of the matrix representing $\\{f,c_{1}\cdot
g_{1},\dots,c_{m}\cdot g_{m}\\}$ $\triangleright$ Proposition 7

5: $\Phi$ $\leftarrow$ $\Phi$ purged of all divisibilities of the form
$f\mathrel{|}g$ for some polynomial $g$

6: for $(a_{d},\dots,a_{1},a_{0})$ non-zero column of $H$ do

7: $\Phi$ $\leftarrow$ $\Phi\land(f\mathrel{|}a_{d}\cdot
x_{d}+\dots+a_{1}\cdot x_{1}+a_{0})$

8:return $\Phi$

Below, let $\Psi$ be the system returned by the algorithm on input $\Phi$.

The fact that $\Psi$ has the elimination property follows from properties of
the Hermite normal form. Consider $F$ defined as in line 1, and $f\in F$.
Starting from the matrix $A\in\mathbb{Z}^{(d+1)\times(m+1)}$ representing the
spanning set $S\coloneqq\\{f,c_{1}\cdot g_{1},\dots,c_{m}\cdot g_{m}\\}$
computed in line 3, by Proposition 6 we conclude that $H$ in line 4 spans
$\textup{M}_{f}(\Phi)$. Moreover, by properties of the HNF, all non-zero
columns of $H$ are linearly independent, hence the for loop in line 6 is
adding divisibilities $f\mathrel{|}h_{1},\dots,f\mathrel{|}h_{\ell}$ where
$h_{1},\dots,h_{\ell}$ is a basis of $\textup{M}_{f}(\Phi)$; and $\ell\leq
m+1$. Note that line 5 has previously removed all divisibilities of the form
$f\mathrel{|}g$. Hence, in $\Psi$ only the divisibilities
$f\mathrel{|}h_{1},\dots,f\mathrel{|}h_{\ell}$ have $f$ as a left-hand side.
Recall now that each column $(a_{d},\dots,a_{1},c)$ of the matrix $A$ contains
the coefficients and the constant of a distinct element $h\in S$, with $a_{i}$
being the coefficient of $x_{i}$ for $i\in[1,d]$, and $c$ being the constant
of $h$. Again since $H$ is in HNF, it is lower triangular, and the pivot of
each non-zero column is strictly below the pivot of the column before it.
Following the order $x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$, this
allows us to conclude that, for every $k\in[0,d]$, the family
$\\{g_{1},\dots,g_{j}\\}\coloneqq\\{g:\textup{LV}(g)\preceq x_{k}\text{ and
}f\mathrel{|}g\text{ appears in }\Psi\\}$ is such that $g_{1},\dots,g_{j}$ are
linearly independent polynomials forming a basis for
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{k}]$; i.e., $\Psi$ has the
elimination property. We also note that, by virtue of the updates done in 7,
Items 1 and 2 in the statement of Lemma 7 directly follow.

The fact that $\Psi$ and $\Phi$ are equivalent both over $\mathbb{Z}$ and for
solutions modulo a prime follows from Items 1 and 2 together with the
following property of divisibility modules: given a system of divisibility
constraints $\Phi^{\prime}$ and a primitive term $f$,

  * •

for every $\boldsymbol{a}$ integer solution of $\Phi^{\prime}$ and every
$g\in\textup{M}_{f}(\Phi^{\prime})$, $f(\boldsymbol{a})$ divides
$g(\boldsymbol{a})$,

  * •

for every $p\in\mathbb{P}$, $\boldsymbol{b}$ solution of $\Phi^{\prime}$
modulo $p$ and every $g\in\textup{M}_{f}(\Phi^{\prime})$,
$v_{p}(f(\boldsymbol{b}))\leq v_{p}(g(\boldsymbol{b}))$.

Here, note that given polynomials $g_{1}$ and $g_{2}$ with
$v_{p}(f(\boldsymbol{b}))\leq v_{p}(g_{1}(\boldsymbol{b}))$ and
${v_{p}(f(\boldsymbol{b}))\leq v_{p}(g_{2}(\boldsymbol{b}))}$ we have
$v_{p}(f(\boldsymbol{b}))\leq v_{p}(a_{1}\cdot
g_{1}(\boldsymbol{b})+a_{2}\cdot g_{2}(\boldsymbol{b}))$ for every
$a_{1},a_{2}\in\mathbb{Z}$, as the $p$-adic evaluation satisfies $v_{p}(x\cdot
y)=v_{p}(x)+v_{p}(y)$ and $\min(v_{p}(x),v_{p}(y))\leq v_{p}(x+y)$, for all
$x,y\in\mathbb{Z}$.

Let us now move to the bounds on $\Psi$ stated in Item 3. Directly from
$\\#F\leq m$ and the fact that $H$ is lower triangular we conclude that at
most $m\cdot(d+1)$ divisibilities are added, and so $\Psi$ has at most
$m\cdot(d+2)$ divisibilities. We analyze the norm of $\Psi$. It suffices to
consider a single $f\in F$. By definition,
${|\mkern-2.0mu|}f{|\mkern-2.0mu|}\leq{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}$,
and from Lemma 6, the infinity norm of the matrix $A$ representing
$\\{f,c_{1}\cdot g_{1},\dots,c_{m}\cdot g_{m}\\}$ is bounded by
$((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)^{3}}\cdot{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}$.
Note that $A$ has $d+1$ many rows. By Proposition 7, the matrix $H$ in line 4
is such that

$\displaystyle{|\mkern-2.0mu|}H{|\mkern-2.0mu|}$
$\displaystyle\leq((d+1)\cdot{|\mkern-2.0mu|}A{|\mkern-2.0mu|}+1)^{O(d)}$
$\displaystyle\leq\Big{(}(d+1)\cdot\big{(}((m+3)\cdot({|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2))^{(m+3)^{3}}\cdot{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\big{)}+1\Big{)}^{O(d)}$
$\displaystyle\leq(d+1)^{O(d)}(m+{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2)^{O(m^{3}d)}.$

From the updates done in line 7, we conclude that
${|\mkern-2.0mu|}\Psi{|\mkern-2.0mu|}\leq(d+1)^{O(d)}(m+{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}+2)^{O(m^{3}d)}$.
∎

See 8

###### Proof.

Let $f$ be a primitive polynomial. By definition of divisibility module, the
lemma is true as soon as we prove  (i)
$f\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$,
(ii) $\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$is
a $\mathbb{Z}$-module, and  (iii) for every divisibility
$g^{\prime}\mathrel{|}h^{\prime}$ (with $g^{\prime}$ non-zero) appearing in
$\Phi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$, if $b\cdot
g^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$
for some $b\in\mathbb{Z}$, then $b\cdot
h^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$.
Indeed, by definition
$\textup{M}_{f}(\Phi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$ is the
smallest set fulfilling these three properties, and therefore it must then be
included in
$\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$.

The first two properties trivially follow by definition of
$\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$, hence
let us focus on Property (iii). Consider a divisibility
$g^{\prime}\mathrel{|}h^{\prime}$ appearing in
$\Phi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and such that $b\cdot
g^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$.
By definition of $\Phi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$,
there is a divisibility $g\mathrel{|}h$ appearing in $\Phi$ such that
${(g\mathrel{|}h)[\boldsymbol{\nu}(\boldsymbol{x})\mathbin{/}\boldsymbol{x}]=(g^{\prime}\mathrel{|}h^{\prime})}$.
We split the proof depending on whether $g$ is a primitive polynomial.

$g$ is not a primitive polynomial.

By Item 1 in Lemma 7 the divisibility $g\mathrel{|}h$ occurs in $\Psi$. So,
$g^{\prime}\mathrel{|}h^{\prime}$ is in
$\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and directly by
definition of divisibility module, $b\cdot
h^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$.

$g$ is a primitive polynomial.

Let $\widetilde{g}$ and $c^{\prime}\in\mathbb{Z}\setminus\\{0\\}$ be such that
$g^{\prime}=c^{\prime}\cdot\widetilde{g}$. By Item 2 in Lemma 7, since
$g\mathrel{|}h$ appears in $\Phi$, $h\in\textup{M}_{g}(\Psi)$. By the
elimination property of $\Psi$, there are divisibilities
$g\mathrel{|}h_{1},\dots,g\mathrel{|}h_{k}$ such that $h=\lambda_{1}\cdot
h_{1}+\dots+\lambda_{k}\cdot h_{k}$ for some
$\lambda_{1},\dots,\lambda_{k}\in\mathbb{Z}\setminus\\{0\\}$. Every
divisibility
$(g\mathrel{|}h_{i})[\boldsymbol{\nu}(\boldsymbol{x})\mathbin{/}\boldsymbol{x}]$
with $i\in[1,k]$ appears in
$\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$. Since
$g^{\prime}=g(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and $b\cdot
g^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$
we have $b\cdot
h_{i}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$
for every $i\in[1,k]$. Note that
$h^{\prime}=h(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})=\lambda_{1}\cdot
h_{1}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})+\dots+\lambda_{k}\cdot
h_{k}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$, and therefore since
the divisibility module is a $\mathbb{Z}$-module, $b\cdot
h^{\prime}\in\textup{M}_{f}(\Psi(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y}))$.
∎

##  Appendix D Bounding the number of difficult primes

In this appendix, we establish Lemmas 3, 9 and 4.

See 3

###### Proof.

We remark that $p$ not dividing any coefficients nor constants appearing in
the left-hand sides of $\Phi$ implies that all the left-hand sides are non-
zero. We show that the system of non-congruences defined by $f_{i}\not\equiv
0\pmod{p}$ for every $i\in[1,m]$, admits a solution $\boldsymbol{b}$. This
solution can clearly be taken with entries in $[0,p-1]$. Furthermore,
$v_{p}(f_{i}(\boldsymbol{b}))=0$ and $f_{i}(\boldsymbol{b})\neq 0$ for every
$i\in[1,m]$, and therefore $\boldsymbol{b}$ is a solution for $\Phi$ modulo
$p$ no matter the values of $v_{p}(g_{i}(\boldsymbol{b}))$ ($i\in[1,m]$).

Consider an arbitrary ordering $x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$
on the variables in $\boldsymbol{x}$. We construct $\boldsymbol{b}$ by
induction on $k\in[0,d]$. At the $k$-th step of the induction we deal with the
linear terms $h$ having ${\textup{LV}(h)=x_{k}}$. Below, we write $F_{0}$ for
the set of the left-hand sides in $\Phi$ that are constant polynomials, and
$F_{k}$ with $k\in[1,d]$ for the set of the left-hand sides $f$ in $\Phi$ such
that $\textup{LV}(f)\preceq x_{k}$.

base case: $k=0$.

Every $f\in F_{0}$ is a non-zero integer. Then, $f\not\equiv 0\pmod{p}$
directly follows from the hypothesis that $p$ does not divide any constant
appearing in the left-hand sides of $\Phi$.

induction step: $k\geq 1$.

From the induction hypothesis, there is
$\boldsymbol{b}_{k-1}=(b_{1},\dots,b_{k-1})\in\mathbb{Z}^{k-1}$ such that for
every $f\in F_{k-1}$, $f(\boldsymbol{b}_{k-1})\not\equiv 0\pmod{p}$. We find a
value $b_{k}$ for $x_{k}$ so that the following system of non-congruences is
satisfied

$\displaystyle f(\boldsymbol{b}_{k-1},x_{k})\not\equiv 0\pmod{p}$
$\displaystyle f\in F_{k}\setminus F_{k-1}.$

Linear polynomials $f$ in $F_{k}\setminus F_{k-1}$ are of the form
$f(\boldsymbol{x})=f^{\prime}(x_{1},\dots,x_{k-1})+c_{f}\cdot x_{k}$. Since by
hypothesis $p\nmid c_{f}$, we consider the multiplicative inverse $c_{f}^{-1}$
of $c_{f}$ modulo $p$, and rewrite the above system as $x_{k}\not\equiv-
c_{f}^{-1}\cdot f^{\prime}$ for every $f\in F_{k}\setminus F_{k-1}$. This
system as a solution directly from the fact that $p>m\geq\\#(F_{k}\setminus
F_{k-1})$. ∎

Before proving Lemmas 9 and 4, we need the following result on system of
divisibility constraints with the elimination property, that will later be
used also in the proof of 4.

######  Lemma 19.

Let $\Phi(x_{1},\dots,x_{d})$ be a system of divisibility with the elimination
property for the order $x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$. For
every primitive term $f$ and $j\in[1,d]$, the set
$F\coloneqq\\{g:{(f\mathrel{|}g)}\text{ appears in }\Phi\\}$ has at most one
element with leading variable $x_{j}$.

###### Proof.

If $f$ does not appear in the left-hand side of a divisibility of $\Phi$, then
$F=\emptyset$ and the lemma holds. Suppose $f$ in a left-hand side. For
simplicity, let us define $x_{0}\coloneqq\bot$. By definition, for every
${k\in[0,d]}$, the elimination property forces
$\\{g_{1},\dots,g_{\ell}\\}\coloneqq\\{g:{\textup{LV}(g)\preceq x_{k}}\text{
and }{f\mathrel{|}g}\text{ appears in }\Phi\\}$ to be such that
$g_{1},\dots,g_{\ell}$ are linearly independent polynomials forming a basis
for $\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{k}]$. Given
$k\in[0,d]$, let us write $F_{k}\coloneqq\\{g:\textup{LV}(g)\preceq
x_{k}\text{ and }(f\mid g)\text{ appear in }\Phi\\}$. For $j\in[1,d]$, by the
elimination property, $F_{j-1}$ and $F_{j}$ are sets of linearly independent
vectors, that respectively generates
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{j-1}]$ and
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{j}]$. To conclude the
proof, we show by induction on $j$ that the set $F_{j}$ has at most one
element with leading variable $x_{j}$.

base case $j=0$.

In this case $F_{0}$ only contains constant polynomials (and might be empty,
in that case it generates the subspace $\\{0\\}$). By elimination property,
$F$ is a set of linearly independent vectors, hence $F_{0}$ contains at most
one element.

induction step $j\geq 1$.

_Ad absurdum_ , suppose there are two distinct $g_{1},g_{2}\in F_{j}\setminus
F_{j-1}$ such that $\textup{LV}(g_{1})=\textup{LV}(g_{2})=x_{j}$. By
definition of $S$-polynomial,
$S(g_{1},g_{2})\in\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{j-1}]$.
Since $F_{j-1}$ generates
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{j-1}]$, there is a sequence
of integers $(\lambda_{h})_{h\in F_{j-1}}$ such that $\sum_{h\in
F_{j-1}}\lambda_{h}\cdot h=S(g_{1},g_{2})$. However,
$F_{j-1}\cup\\{g_{1},g_{2}\\}\subseteq F_{j}$ (by definition) and $F_{j}$ is a
set of linearly independent vectors. Therefore, every $\lambda_{h}$ above must
be $0$, and we obtain $S(g_{1},g_{2})=0$, i.e., $g_{1}$ and $g_{2}$ are
linearly dependent, in contradiction with $g_{1},g_{2}\in F_{j}$. ∎

See 9

###### Proof.

Consider a primitive term $f$. If $f$ is not a primitive part of any $f_{i}$,
with $i\in[1,m]$, then $\mathrm{S}_{f}(\Phi)=\textup{terms}(\Phi)$ and so
$\mathrm{S}_{f}(\Phi)$ is included in any $\mathrm{S}_{f^{\prime}}(\Phi)$
where $f^{\prime}$ is a primitive part of a left-hand side of $\Phi$. Hence,
we can upper bound $\\#\Delta(\Phi)$ and
$\langle{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\rangle$ by only looking at these
primitive parts.
Proof of i: For $f$ primitive part of some polynomials in a left-hand side of
$\Phi$, the elements of $\mathrm{S}_{f}(\Phi)$ have the form
$S\big{(}g_{k},S(g_{k-1},\dots S(g_{1},h))\big{)}$ where
$h\in\textup{terms}(\Phi)$ and $f\mid g_{i}$ is a divisibility in $\Phi$, for
all $i\in[1,k]$. Moreover, each $g_{i}$ has the same leading variable as
$h_{i}\coloneqq S(g_{i-1},S(g_{i-2},\dots,S(g_{1},h)))$. Since $\Phi$ has the
elimination property, by Lemma 19, given $h_{i}$ there is at most one $g$ such
that $f\mathrel{|}g$ and $\textup{LV}(g)=\textup{LV}(h_{i})$; that is $g_{i}$.
Therefore, each element of $\mathrm{S}_{f}(\Phi)$ can be characterized by a
pair $(k,h)$ where $h\in\textup{terms}(\Phi)$ and $k\in[0,d+1]$, i.e.,
$\\#\mathrm{S}_{f}(\Phi)\leq\\#\textup{terms}(\Phi)\cdot(d+2)\leq 2\cdot
m\cdot(d+2)$, since $\\#\textup{terms}(\Phi)\leq 2\cdot m$. The number of $f$
to be considered is bounded by $m$, i.e., the number of left-hand sides, which
means $\\#\Delta(\Phi)\leq 2\cdot m^{2}(d+2)$.
Proof of ii: Recall that $\langle{|\mkern-2.0mu|}f{|\mkern-2.0mu|}\rangle$ is
the maximum bit length of a coefficient or constant of a polynomial $f$, and
that $\langle{|\mkern-2.0mu|}R{|\mkern-2.0mu|}\rangle=\max_{f\in
R}\langle{|\mkern-2.0mu|}f{|\mkern-2.0mu|}\rangle$ for a finite set $R$ of
polynomials. By examinating the definition of $S$-polynomial, we get that for
every $f$ and $g$,
${\langle{|\mkern-2.0mu|}S(f,g){|\mkern-2.0mu|}\rangle}\leq{\langle{|\mkern-2.0mu|}f{|\mkern-2.0mu|}\rangle}+{\langle{|\mkern-2.0mu|}g{|\mkern-2.0mu|}\rangle}+1$.
Let $f$ be a primitive polynomial. As discussed in the proof of (i), an
element of $\mathrm{S}_{f}(\Phi)$ is of the form
$S\big{(}g_{k},S(g_{k-1},\dots S(g_{1},h))\big{)}$, where
$h\in\textup{terms}(\Phi)$, $f\mid g_{i}$ is a divisibility in $\Phi$, for all
$i\in[1,k]$, and $k\leq d+1$. Then,
$\langle{|\mkern-2.0mu|}S\big{(}g_{k},S(g_{k-1},\dots
S(g_{1},h))\big{)}{|\mkern-2.0mu|}\rangle\leq\langle{|\mkern-2.0mu|}h{|\mkern-2.0mu|}\rangle+\big{(}\sum_{i=1}^{k}\langle{|\mkern-2.0mu|}g_{i}{|\mkern-2.0mu|}\rangle\big{)}+k$.
We conclude that
$\langle{|\mkern-2.0mu|}\Delta(\Phi){|\mkern-2.0mu|}\rangle\leq(d+2)\cdot(\langle{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\rangle+1)$.
∎

See 4

###### Proof.

We first analyse $\log_{2}(\Pi\mathbb{P}(\Phi))$. Recall that
$\mathbb{P}(\Phi)$ is the set of those primes $p$ such that either (i) $p\leq
m$ or (ii) $p$ divide a coefficient or a constant of a left-hand side of
$\Phi$. The product of the primes satisfying (i) is bounded by $m!\leq m^{m}$.
The product of the primes satisfying (ii) is bounded by the product of the
coefficients or the constants in the left-hand sides of $\Phi$, which is at
most ${|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}^{m\cdot(d+1)}$. From these two
bounds, we obtain the bound on $\log_{2}(\Pi\mathbb{P}(\Phi))$ stated in the
lemma.

Let us analyse $\log_{2}(\Pi\mathbf{P}_{\\!\\!+}(\Phi))$. Without loss of
generality, assume that the order $\mathbin{\prec}$ is such that
${x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}}$. We consider the three
conditions defining $\mathbf{P}_{\\!\\!+}(\Phi)$ separately, and establish
upper bounds for each of them. Recall that the number of primes dividing
$n\in\mathbb{Z}$ is bounded by $\log_{2}(n)$, and that Lemma 9 implies
$\\#S(\Delta(\Phi))\leq 8\cdot m^{4}(d+2)^{2}$ and
$\langle{|\mkern-2.0mu|}S(\Delta(\Phi)){|\mkern-2.0mu|}\rangle\leq
2\cdot(d+2)\cdot(\langle{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\rangle+1)+1$.

(P1):

Directly from the bounds above, the primes satisfying (P1) are at most
${8\cdot m^{4}(d+2)^{2}}$, and thus the $\log_{2}$ of their product is at most
${8\cdot m^{4}(d+2)^{2}\log_{2}(8\cdot m^{4}(d+2)^{2})}$, which is bounded by
${64\cdot m^{5}(d+2)^{3}}$.

(P2):

The product of the primes dividing a coefficient or constant of a polynomial
$f$ in $S(\Delta(\Phi))$ is bounded by the product of these coefficients and
constants. There are at most $(d+1)\cdot\\#S(\Delta(\Phi))$ such coefficients
and constants. Therefore, the $\log_{2}$ of this product is bounded by
$(d+1)\cdot\\#S(\Delta(\Phi))\cdot\langle{|\mkern-2.0mu|}S(\Delta(\Phi)){|\mkern-2.0mu|}\rangle$,
which is bounded by ${16\cdot
m^{4}(d+2)^{4}(\langle{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\rangle+2)}$.

(P3):

If $f$ is a primitive term such that $a\cdot f$ does not occur in the left-
hand sides of $\Phi$, for any $a\in\mathbb{Z}\setminus\\{0\\}$, then
$\mathrm{S}_{f}(\Phi)=\textup{terms}(\Phi)$ and
$\textup{M}_{f}(\Phi)=\mathbb{Z}f$, and therefore $\lambda$, if it exists,
equals to $1$. Consider $f$ primitive such that $a\cdot
f\in\textup{terms}(\Phi)$ appears on the left-hand side of a divisibility in
$\Phi$, for some $a\in\mathbb{Z}\setminus\\{0\\}$, and consider
$g\in\mathrm{S}_{f}(\Phi)$. We first compute a bound on the minimal positive
$\lambda$ such that $\lambda\cdot g\in\textup{M}_{f}(\Phi)$, if such a
$\lambda$ exists. Let $x_{j}\coloneqq\textup{LV}(g)$, with $j\in[0,d]$ and
$x_{0}\coloneqq\bot$. Consider the set
$\\{h_{1},\dots,h_{\ell}\\}\coloneqq\\{h:\textup{LV}(h)\leq\textup{LV}(g)\text{
and }f\mathrel{|}h\text{ is in }\Phi\\}$; where $\ell\leq m$. From the
elimination property, this set is a basis for
$\textup{M}_{f}(\Phi)\cap\mathbb{Z}[x_{1},\dots,x_{j}]$, and therefore
$\lambda$ exists if and only if
${\mathbb{Z}g\cap\mathbb{Z}h_{1}+\dots+\mathbb{Z}h_{\ell}\neq\\{0\\}}$. Then
let $K$ be a basis for the kernel of the matrix representing the set
$\\{-g,h_{1},\dots,h_{\ell}\\}$. As observed in the context of Algorithm 4, if
$\lambda$ exists then it is the GCD of the row of $K$ corresponding to $-g$.
From Corollary 2,
$\lambda\leq\big{(}m+3)^{m+3}\max(2,{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|})^{m+2}$.
In the proof of Lemma 9 we have shown $\\#\mathrm{S}_{f}(\Phi)\leq 2\cdot
m\cdot(d+2)$, hence the number of pairs $(f,g)$ to consider is bounded by
$2\cdot m^{2}\cdot(d+2)$. Similarly to (P2), the product of the primes
dividing all $\lambda$s is bounded by the product of these $\lambda$s, which
is at most
$\big{(}(m+3)^{m+3}\max(2,{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|})^{m+2}\big{)}^{2\cdot
m^{2}\cdot(d+2)}$. Therefore, the $\log_{2}$ of the product of the primes
satisfying (P3) is at most $32\cdot
m^{4}(d+2)\cdot(\langle{|\mkern-2.0mu|}\Phi{|\mkern-2.0mu|}\rangle+1)$.

Summing up the bounds we have just obtained yield the bound stated in the
lemma. ∎

##  Appendix E Theorem 4: proofs of 4 and 5

In this section, we prove 4 and 5, which are required to establish Theorem 4.
In the context of this theorem, recall that
$\Psi(\boldsymbol{x},\boldsymbol{y})$ is a formula that is increasing for
$(X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$ and has the elimination
property for an order
$(\mathbin{\prec})\in(X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$. Here,
$\boldsymbol{x}=(x_{1},\dots,x_{d})$ are the variables appearing in $X_{1}$,
ordered as $x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}$, and
$\boldsymbol{y}$ are the variables appearing in $\bigcup_{j=2}^{r}X_{j}$. We
also have solutions $\boldsymbol{b}_{p}$ for $\Psi$ modulo $p$, for every
$p\in\mathbf{P}_{\\!\\!+}(\Psi)$, and we have inductively computed a map
$\boldsymbol{\nu}\colon X_{1}\to\mathbb{Z}$ the following three properties:

IH1:

For every $p\in\mathbf{P}_{\\!\\!+}(\Psi)$ and $x\in X_{1}$,
$\boldsymbol{\nu}(x)\equiv b_{p,x}\pmod{p^{\mu_{p}+1}}$, where $b_{p,x}$ is
the entry of $\boldsymbol{b}_{p}$ corresponding to $x$, and
$\mu_{p}\coloneqq\max\\{v_{p}(f(\boldsymbol{b}_{p}))\in\mathbb{N}:f\text{ is
in the left-hand side of a divisibility of }\Psi\\}$.

IH2:

For every prime $p\notin\mathbf{P}_{\\!\\!+}(\Psi)$ and for every
$h,h^{\prime}\in\Delta(\Psi)$ with leading variable in $X_{1}$, if
$S(h,h^{\prime})$ is not identically zero, then $p$ does not divide both
$h(\boldsymbol{\nu}(\boldsymbol{x}))$ and
$h^{\prime}(\boldsymbol{\nu}(\boldsymbol{x}))$.

IH3:

$h(\boldsymbol{\nu}(\boldsymbol{x}))\neq 0$ for every $h\in\Delta(\Psi)$ that
is non-zero and with $\textup{LV}(h)\in X_{1}$.

The formula $\Psi^{\prime}(\boldsymbol{y})$ considered in 4 and 5 is defined
as $\Psi^{\prime}\coloneqq\Psi[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X_{1}]$.

See 4

At first glance, 4 might appear intuitively true: since the notion of
$r$-increasing form is mainly a property on sets
$X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r}$ of orders of variables, and
during the proof of Theorem 4 we are inductively handling the smallest set
$X_{1}$, it might seem trivial that instantiating the variables in $X_{1}$
preserve increasingness for $X_{2}\mathbin{\prec}\dots\mathbin{\prec}X_{r}$.
However, in general, this is not the case. To see this, we repropose the
example given in Section 1.3. Consider the system of divisibility constraints
$\Psi$ in increasing form for the order
$u\mathbin{\prec}v\mathbin{\prec}x\mathbin{\prec}y\mathbin{\prec}z$ and with
the elimination property for that order:

$\displaystyle v$ $\displaystyle\mathrel{|}u+x+y$ $\displaystyle v$
$\displaystyle\mathrel{|}x$ $\displaystyle y+2$ $\displaystyle\mathrel{|}z+1$
$\displaystyle v$ $\displaystyle\mathrel{|}z\,.$

From the first two divisibilities, we have $(u+y)\in\textup{M}_{v}(\Psi)$;
i.e., $(u-2)+(y+2)\in\textup{M}_{v}(\Psi)$. Therefore, if $u$ were to be
instantiated as $2$, the resulting formula $\Psi^{\prime}$ would satisfy
$(y+2)\in\textup{M}_{v}(\Psi^{\prime})$ and hence
$(z+1)\in\textup{M}_{v}(\Psi^{\prime})$, from the third divisibility. Then,
$1\in\textup{M}_{v}(\Psi^{\prime})$ would follow from the last divisibility,
violating the constraints of the increasing form. Fortunately, due to the
definition of $\mathrm{S}_{f}(\Psi)$, $u=2$ contradicts the property (IH3:)
kept during the proof of Theorem 4, meaning that the above issue does not
occur in our setting. Indeed, note that $S(y+2,u+x+y)=2-u-x$ is in
$\mathrm{S}_{v}(\Psi)$, and so is $S(2-u-x,x)=2-u$. Then, (IH3:) forces
$2-u\neq 0$, excluding $u=2$ as a possible solution. This observation is the
key to establish 4.

Given a set $A$ of polynomials, an integer $a\in\mathbb{Z}$ and a variable $x$
occurring in those polynomials, we define
$A[a\mathbin{/}x]\coloneqq\\{f(a,\boldsymbol{y}):f(x,\boldsymbol{y})\in A\\}$,
that is the set obtained by partially evaluating $x$ as $a$ in all polynomials
in $A$. This notion is extended to sequences of value-variable pairs as
$A[a_{i}\mathbin{/}x_{i}:i\in I]$.

###### Proof of 4.

To show the statement, we consider an order $\mathbin{\prec}^{\prime}$ in
$(X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$. Note that any order
$(X_{2}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$ can be constructed from
elements in $(X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$ by simply
forgetting $X_{1}$. Let $\boldsymbol{y}=(y_{1},\dots,y_{j})$, with
$y_{1}\mathbin{\prec}^{\prime}\dots\mathbin{\prec}^{\prime}y_{j}$, be the
variables in $\bigcup_{i=2}^{r}X_{i}$. To simplify the presentation, we denote
by $a^{\prime},b^{\prime},\dots$ and $f^{\prime},g^{\prime},\dots$ integers
and polynomials related to $\Psi^{\prime}$, and by $a,b,\dots$ and $f,g,\dots$
integers and polynomials related to $\Psi$. By definition of increasing form,
we need to establish that for every $k\in[1,j]$ and primitive polynomial
$f^{\prime}(\boldsymbol{y})$ such that $a^{\prime}\cdot f^{\prime}$ appears in
the left-hand side of a divisibility in $\Psi^{\prime}$, for some
$a^{\prime}\in\mathbb{Z}\setminus\\{0\\}$, and
$\textup{LV}(f^{\prime})=y_{k}$, we have
$\textup{M}_{f^{\prime}}(\Psi^{\prime})\cap\mathbb{Z}[y_{1},\dots,y_{k}]=\mathbb{Z}f^{\prime}$.
By definition of $\Psi^{\prime}$ and since $a^{\prime}\cdot f^{\prime}$
appears in a left-hand side, there is a primitive polynomial
$f(\boldsymbol{x},\boldsymbol{y})$ and a scalar
$a\in\mathbb{Z}\setminus\\{0\\}$ such that $a\cdot f$ is in the left-hand side
of some divisibility in $\Psi$, and $a^{\prime}\cdot
f^{\prime}(\boldsymbol{y})=a\cdot
f(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$. Note that this implies
$a\mathrel{|}a^{\prime}$ and $\textup{LV}(f)\not\in X_{1}$. We prove that
$\frac{a^{\prime}}{a}\cdot\textup{M}_{f^{\prime}}(\Psi^{\prime})\subseteq\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$. Note that this inclusion implies $\Psi^{\prime}$ in increasing form.
To see this, take
$g^{\prime}\in\textup{M}_{f^{\prime}}(\Psi^{\prime})\cap\mathbb{Z}[y_{1},\dots,y_{k}]$.
We have $\frac{a^{\prime}}{a}\cdot
g^{\prime}\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$, and thus there is
$g(\boldsymbol{x},\boldsymbol{y})\in\textup{M}_{f}(\Psi)$ such that
$\frac{a^{\prime}}{a}\cdot
g^{\prime}=g(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$. Since
$\textup{LV}(g^{\prime})\mathbin{\prec}^{\prime}y_{k}$, we have
$\textup{LV}(g)\mathbin{\prec}^{\prime}y_{k}$. Since $\Psi$ is increasing for
$\mathbin{\prec}^{\prime}$, we conclude that $g\in\mathbb{Z}f$. Note that
$(\mathbb{Z}f)[\boldsymbol{\nu}(x)\mathbin{/}x\in
X_{1}]\subseteq\mathbb{Z}f^{\prime}$. Then $\frac{a^{\prime}}{a}\cdot
g^{\prime}\in\mathbb{Z}f^{\prime}$. Since $f^{\prime}$ is primitive, we get
$g^{\prime}\in\mathbb{Z}f^{\prime}$. This shows
$\textup{M}_{f^{\prime}}(\Psi^{\prime})\cap\mathbb{Z}[y_{1},\dots,y_{k}]\subseteq\mathbb{Z}f^{\prime}$,
and the other inclusion directly follows by definition of
$\textup{M}_{f^{\prime}}(\Psi^{\prime})$. We conclude that $\Psi^{\prime}$ is
increasing.

To conclude the proof of 4, let us show that
$\frac{a^{\prime}}{a}\cdot\textup{M}_{f^{\prime}}(\Psi^{\prime})\subseteq\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$. By definition of $\textup{M}_{f^{\prime}}(\Psi^{\prime})$, this
follows as soon as we prove the following three properties:

  1. (A)

$\frac{a^{\prime}}{a}\cdot f^{\prime}$ belongs to
$\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X_{1}]$,

  2. (B)

$\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X_{1}]$ is a
$\mathbb{Z}$-module, and

  3. (C)

If $g^{\prime}\mathrel{|}h^{\prime}$ is a divisibility in $\Psi^{\prime}$ and
$b^{\prime}\cdot
g^{\prime}\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X_{1}]$
for some $b^{\prime}\in\mathbb{Z}\setminus\\{0\\}$, then $b^{\prime}\cdot
h^{\prime}\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$.

By definition of divisibility module,
$\frac{a^{\prime}}{a}\cdot\textup{M}_{f^{\prime}}(\Psi^{\prime})$ is the
smallest set that satisfies the three properties above, and therefore it must
be included in $\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$.
Proof of A: By definition of $f$, $a^{\prime}\cdot f^{\prime}=a\cdot
f(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and
$a\mathrel{|}a^{\prime}$, hence $\frac{a^{\prime}}{a}\cdot
f^{\prime}=f(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$, and by
definition of divisibility module
$f(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$.
Proof of B: This follows directly from the definition of divisibility module
being a $\mathbb{Z}$-module. Indeed, substitutions preserve the notion of
$\mathbb{Z}$-module.
Proof of C: This property follows from our definition of
$\mathrm{S}_{f}(\Psi)$ together with the property (IH3:) and the fact that
$\Psi$ has the elimination property for the order $\mathbin{\prec}$ (not to be
confused with the order $\mathbin{\prec}^{\prime}$, which does not guarantee
the elimination property). Consider a divisibility
$g^{\prime}(\boldsymbol{y})\mathrel{|}h^{\prime}(\boldsymbol{y})$ occurring in
$\Psi^{\prime}$ and $b^{\prime}\in\mathbb{Z}\setminus\\{0\\}$ such that
$b^{\prime}\cdot
g^{\prime}\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$. By definition of $\Psi^{\prime}$, there is a divisibility
$g(\boldsymbol{x},\boldsymbol{y})\mathrel{|}h(\boldsymbol{x},\boldsymbol{y})$
in $\Psi$ such that
$g^{\prime}=g(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and
$h^{\prime}=h(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$. Also, by
definition of $\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in
X_{1}]$, there is a polynomial
$\widehat{g}(\boldsymbol{x},\boldsymbol{y})\in\textup{M}_{f}(\Psi)$ such that
$b^{\prime}\cdot
g^{\prime}=\widehat{g}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$.

To conclude the proof, it suffices to show that $b^{\prime}\cdot
g=\widehat{g}$. Indeed, since $g\mathrel{|}h$ appears in $\Psi$ and
$\widehat{g}\in\textup{M}_{f}(\Psi)$, we then get $b^{\prime}\cdot
h\in\textup{M}_{f}(\Psi)$ by the definition of divisibility module, which
implies $b^{\prime}\cdot
h^{\prime}\in\textup{M}_{f}(\Psi)[\boldsymbol{\nu}(x)\mathbin{/}x:x\in X_{1}]$
by definition of $h$; concluding the proof.

Since $\widehat{g}\in\textup{M}_{f}(\Psi)$ and $\Psi$ has the elimination
property for $\mathbin{\prec}$, there are linearly independent polynomials
$h_{1},\dots,h_{\ell}$ such that the divisibilities $f\mathrel{|}h_{i}$ appear
in $\Psi$ and there are
${\lambda_{1},\dots,\lambda_{\ell}\in\mathbb{Z}\setminus\\{0\\}}$ such that
$\widehat{g}=\sum_{i=1}^{\ell}\lambda_{i}\cdot h_{i}$. Thanks to Lemma 19, we
can arrange these polynomials so that
$\textup{LV}(h_{1})\mathbin{\prec}\dots\mathbin{\prec}\textup{LV}(h_{\ell})$.
We write $c_{i}$ for the coefficient corresponding to the leading variable of
$h_{i}$. Since $\textup{LV}(f)\not\in X_{1}$ (stated earlier) and $\Psi$ is
increasing, ${\textup{LV}(h_{i})\in\bigcup_{k=2}^{r}X_{k}}$ holds for every
$i\in[1,\ell]$. From
$g^{\prime}=g(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ and
$b^{\prime}\cdot
g^{\prime}=\widehat{g}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$ we
directly get $b^{\prime}\cdot
g(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})=\widehat{g}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})$.
Therefore, $(b^{\prime}\cdot
g-\widehat{g})(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})=0$, implying
that $b^{\prime}\cdot g-\widehat{g}$ is either constant or has its leading
variable in $X_{1}$. This implies that $b^{\prime}\cdot
g-\sum_{i=1}^{\ell}\lambda_{i}\cdot h_{i}$ is either constant or has its
leading variable in $X_{1}$. Since the $\lambda_{i}$ are non-zero, and
moreover $\textup{LV}(h_{i})$ is not in $X_{1}$ and
$\textup{LV}(h_{1})\mathbin{\prec}\dots\mathbin{\prec}\textup{LV}(h_{\ell})$,
we have $\textup{LV}(b^{\prime}\cdot g-\sum_{i=k+1}^{\ell}\lambda_{i}\cdot
h_{i})=\textup{LV}(h_{k})$ for every $k\in[1,\ell]$, and the coefficient
corresponding to the leading variable of $b^{\prime}\cdot
g-\sum_{i=k+1}^{\ell}\lambda_{i}\cdot h_{i}$ is exactly $\lambda_{k}\cdot
c_{k}$.

We show by induction on $k\in[1,\ell+1]$, with base case $k=\ell+1$, that
$\alpha_{k}\cdot(b^{\prime}\cdot g-\sum_{i=k}^{\ell}\lambda_{i}\cdot
h_{i})=b^{\prime}\cdot S(g,h_{\ell},\dots,h_{k})$, where
$\alpha_{k}\coloneqq\prod_{i=k}^{\ell}c_{i}$, and $S(f_{1},\dots,f_{n})$ is
short for $S(\dots(S(f_{1},f_{2}),\dots),f_{n})$; e.g.,
$S(f_{1},f_{2},f_{3})=S(S(f_{1},f_{2}),f_{3})$.

base case $k=\ell+1$:

For the base case, $\alpha_{\ell+1}=1$ and the equivalence becomes
$b^{\prime}\cdot g=b^{\prime}\cdot g$.

induction step $k\leq\ell$:

we have ${\alpha_{k+1}(b^{\prime}\cdot g-\sum_{i=k+1}^{\ell}\lambda_{i}\cdot
h_{i})=b^{\prime}\cdot S(g,h_{\ell},\dots,h_{k+1})}$ by induction hypothesis.
Note that, from the left-hand side of this equation, the coefficient
corresponding to the leading variable of $b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{k+1})$ is $c_{k}\cdot\alpha_{k+1}\cdot\lambda_{k}$.
Then,

$\displaystyle\alpha_{k}\cdot(b^{\prime}\cdot
g-\sum_{i=k}^{\ell}\lambda_{i}\cdot h_{i})$ $\displaystyle=\ $ $\displaystyle
c_{k}\cdot\alpha_{k+1}(b^{\prime}\cdot g-\sum_{i=k}^{\ell}\lambda_{i}\cdot
h_{i})$ $\displaystyle\text{definition of}~{}\alpha_{k}$ $\displaystyle=\ $
$\displaystyle c_{k}\cdot\alpha_{k+1}(b^{\prime}\cdot
g-\sum_{i=k+1}^{\ell}\lambda_{i}\cdot
h_{i})-c_{k}\cdot\alpha_{k+1}\cdot\lambda_{k}\cdot h_{k}$ $\displaystyle=\,$
$\displaystyle c_{k}\cdot(b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{k+1}))-(c_{k}\cdot\alpha_{k+1}\cdot\lambda_{k})\cdot
h_{k}$ induction hypothesis $\displaystyle=\,$ $\displaystyle
S(b^{\prime}\cdot S(g,h_{\ell},\dots,h_{k+1}),h_{k})$
$\displaystyle\text{coeff.~{}leading var.}~{}h_{k}~{}\text{is}~{}c_{k}$
$\displaystyle\text{coeff.~{}leading var.}~{}(b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{k+1}))~{}\text{is}~{}c_{k}\cdot\alpha_{k+1}\cdot\lambda_{k}$
$\displaystyle=\,$ $\displaystyle b^{\prime}\cdot S(g,h_{\ell},\dots,h_{k})$
$\displaystyle S(b^{\prime}\cdot f_{1},f_{2})=b^{\prime}\cdot
S(f_{1},f_{2}),\text{by definition of }S\text{-polynomial}.$

Thanks to the equality $\alpha_{k}\cdot(b^{\prime}\cdot
g-\sum_{i=k}^{\ell}\lambda_{i}\cdot h_{i})=b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{k})$ we just established, we conclude that
$\alpha_{1}\cdot(b^{\prime}\cdot g-\widehat{g})=b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{1})$. Moreover, from $\textup{LV}(b^{\prime}\cdot
g-\sum_{i=k+1}^{\ell}\lambda_{i}\cdot h_{i})=\textup{LV}(h_{k})$ we conclude
that $\textup{LV}(S(g,h_{\ell},\dots,h_{k+1}))=\textup{LV}(h_{k})$, for every
$k\in[1,\ell]$. Then, since ${g\in\textup{terms}(\Psi)}$ and the
divisibilities ${f\mathrel{|}h_{1}},\,\dots,\,{f\mathrel{|}h_{\ell}}$ appear
in $\Psi$, by definition of $\mathrm{S}_{f}(\Psi)$, we conclude that
${S(g,h_{\ell},\dots,h_{1})\in\mathrm{S}_{f}(\Psi)}$. Recall that
$b^{\prime}\cdot g-\widehat{g}$ is either constant or has its leading variable
in $X_{1}$. The same is true for $S(g,h_{\ell},\dots,h_{1})$, and we have
$(\alpha_{1}\cdot(b^{\prime}\cdot
g-\widehat{g}))(\boldsymbol{\nu}(\boldsymbol{x}))=b^{\prime}\cdot
S(g,h_{\ell},\dots,h_{1})(\boldsymbol{\nu}(\boldsymbol{x}))$. From
$(b^{\prime}\cdot
g-\widehat{g})(\boldsymbol{\nu}(\boldsymbol{x}))=(b^{\prime}\cdot
g-\widehat{g})(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{y})=0$ and
$b^{\prime}\neq 0$ we get
${S(g,h_{\ell},\dots,h_{1})(\boldsymbol{\nu}(\boldsymbol{x}))=0}$. From the
property (IH3:), this can only occur when $S(g,h_{\ell},\dots,h_{1})=0$, and
so $\alpha_{1}\cdot(b^{\prime}\cdot g-\widehat{g})=0$. By definition
$\alpha_{1}\neq 0$, and therefore $b^{\prime}\cdot g=\widehat{g}$, concluding
the proof of (C). ∎

See 5

###### Proof.

The first statement of the claim follows from (IH1:) and the definition of
$\mu_{p}$ (the reasoning is analogous to the one in the base case $r=1$ of the
induction of Theorem 4). For the second statement, consider a prime $p$ not
belonging to $\mathbf{P}_{\\!\\!+}(\Psi)$. We provide a solution
$\boldsymbol{b}_{p}$ for $\Psi^{\prime}(\boldsymbol{y})$ modulo $p$. Let
$\boldsymbol{y}=(y_{1},\dots,y_{j})$ with
$y_{1}\mathbin{\prec}\dots\mathbin{\prec}y_{j}$. To compute
$\boldsymbol{b}_{p}=(b_{p,1},\dots,b_{p,j})$, where $b_{p,k}$ is the value
assigned to $y_{k}$, we consider two cases that depend on whether $p$ divides
some $\alpha_{i}$ appearing in the first block of divisibilities of Equation 7
(i.e., these are the $\alpha_{i}$ with $i\in[\ell+1,n]$).

case $p\nmid\alpha_{i}$ for all $i\in[\ell+1,n]$.

This case is relatively simple. Starting from $y_{1}$ and proceeding in
increasing order of variables, we compute $b_{p,k+1}$ ($k\in\mathbb{N}$) by
solving the system

$\displaystyle h(b_{p,1},\dots,b_{p,k},\,y_{k+1})$ $\displaystyle\not\equiv 0$
$\displaystyle\pmod{p}$ $\displaystyle h\in\textup{terms}(\Psi^{\prime})\text{
s.t.}~{}\textup{LV}(h)=y_{k+1}.$ (13)

With respect to the $h$ above, let us write
$h(b_{p,1},\dots,b_{p,k}\,y_{k+1})=c_{h}+a_{h}\cdot y_{k+1}$ where $c_{h}$ is
the constant term obtained by partially evaluating $h$ with respect to
$(b_{p,1},\dots,b_{p,k})$ and $a_{h}$ is the coefficient of $y_{k+1}$ in $h$.
By definition of $\Psi^{\prime}$, the term $h$ is obtained by substituting
$\boldsymbol{x}$ for $\boldsymbol{\nu}(\boldsymbol{x})$ in a polynomial of
$\Psi$, and in that polynomial $y_{k+1}$ has coefficient $a_{h}$. Since
$p\not\in\mathbf{P}_{\\!\\!+}(\Psi)$, from Condition (P2) we conclude that
$p\nmid a_{h}$, and so $a_{h}$ has an inverse $a_{h}^{-1}$ modulo $p$. The
system of non-congruences above is equivalent to the system
$\mathcal{S}_{k+1}$ given by

$\displaystyle y_{k+1}$ $\displaystyle\not\equiv-a_{h}^{-1}\cdot c_{h}$
$\displaystyle\pmod{p}$ $\displaystyle h\in\textup{terms}(\Psi^{\prime})\text{
s.t.}~{}\textup{LV}(h)=y_{k+1}.$

From Condition (P1) we have
$p>\\#\textup{terms}(\Psi)\geq\\#\textup{terms}(\Psi^{\prime})$, and so it
suffices to take $b_{p,k+1}$ to be an element in $[0,p-1]$ that differs from
every $-a_{h}^{-1}\cdot c_{h}$ appearing in the rows of $\mathcal{S}_{k+1}$.

The solution $\boldsymbol{b}_{p}$ resulting from the systems of non-
congruences $\mathcal{S}_{1},\dots,\mathcal{S}_{j}$ is such that, for every
$h\in\textup{terms}(\Psi^{\prime})$, $v_{p}(h(\boldsymbol{b}_{p}))=0$.
Therefore, $\boldsymbol{b}_{p}$ is a solution for $\Psi^{\prime}$ modulo $p$.

case $p\mathrel{|}\alpha_{i}$ for some $i\in[\ell+1,n]$.

This case is involved. Since $p$ divides some
$\alpha_{i}=f_{i}(\boldsymbol{\nu}(\boldsymbol{x}))$, and
$p\not\in\mathbf{P}_{\\!\\!+}(\Psi)$, by Condition (P2) we have
$p\mathrel{|}f(\boldsymbol{\nu}(\boldsymbol{x}))$, where $f$ is the primitive
polynomial obtained by dividing every coefficient and constant of $f_{i}$ by
$\gcd(f_{i})$. Recall that $\boldsymbol{x}=(x_{1},\dots,x_{d})$ with
$x_{1}\mathbin{\prec}\dots\mathbin{\prec}x_{d}\mathbin{\prec}y_{1}\mathbin{\prec}\dots\mathbin{\prec}y_{j}$,
and note that $\textup{LV}(f)\preceq x_{d}$. Below, let us define $u\coloneqq
v_{p}(f(\boldsymbol{\nu}(\boldsymbol{x})))$. The idea is to use $f$ to
iteratively construct the solution $\boldsymbol{b}_{p}$ for
$\boldsymbol{y}=(y_{1},\dots,y_{j})$. We rely on the following induction
hypotheses ($k\in[0,j]$):

IH1′:

for every non-zero polynomial
$g(\boldsymbol{x},y_{1},\dots,y_{t})\in\textup{terms}(\Psi)$ such that $t\leq
k$,

. if $\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$ then
$v_{p}(g(\boldsymbol{\nu}(\boldsymbol{x}),b_{p,1},\dots,b_{p,t}))=u$, and

IH2′:

for every non-zero polynomial
$h(\boldsymbol{x},y_{1},\dots,y_{t})\in\mathrm{S}_{f}(\Psi)$ such that $t\leq
k$,

. if $\mathbb{Z}h\cap\textup{M}_{f}(\Psi)=\\{0\\}$ then
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x}),b_{p,1},\dots,b_{p,t}))=0$.

Let us first show that by constructing $\boldsymbol{b}_{p}$ so that it
satisfies the hypotheses above for $k=j$ implies that $\boldsymbol{b}_{p}$ is
a solution for $\Psi^{\prime}$ modulo $p$. Consider a divisibility
$\alpha_{i}+f_{i}^{\prime}(\boldsymbol{y})\mid\beta_{i}+g_{i}^{\prime}(\boldsymbol{y})$
in $\Psi^{\prime}$, with $i\in[\ell+1,m]$ and $f_{i}^{\prime}=0$ if $i\leq n$.
Recall that $\alpha_{i}=f_{i}(\boldsymbol{\nu}(\boldsymbol{x}))$ and
$\beta_{i}=g_{i}(\boldsymbol{\nu}(\boldsymbol{x}))$, and given $h\coloneqq
f_{i}+f_{i}^{\prime}$ and $h^{\prime}\coloneqq g_{i}+g_{i}^{\prime}$, the
divisibility $h\mathrel{|}h^{\prime}$ occurs in $\Psi$. We have two cases:

  * •

$\mathbb{Z}h\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$. In this case, by definition
of $\textup{M}_{f}(\Psi)$ we have
$\mathbb{Z}h^{\prime}\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$. According to
(IH1′:),
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{b}_{p}))=v_{p}(h^{\prime}(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{b}_{p}))=u$.
By definition of $h$ and $h^{\prime}$, we get
$v_{p}(\alpha_{i}+f_{i}^{\prime}(\boldsymbol{b}_{p}))=v_{p}(\beta_{i}+g_{i}^{\prime}(\boldsymbol{b}_{p}))=u$.
Note that $f(\boldsymbol{\nu}(\boldsymbol{x}))$ is non-zero by (IH3:), hence
its $p$-adic evaluation $u$ belongs to $\mathbb{N}$, which forces
$\alpha_{i}+f_{i}^{\prime}(\boldsymbol{b}_{p})$ to be non-zero.

  * •

$\mathbb{Z}h\cap\textup{M}_{f}(\Psi)=\\{0\\}$. Recall that
$\textup{terms}(\Psi)\subseteq\mathrm{S}_{f}(\Psi)$, by definition. Hence,
directly from (IH2′:) we get
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x}),\boldsymbol{b}_{p}))=v_{p}(\alpha_{i}+f_{i}^{\prime}(\boldsymbol{b}_{p}))=0$.
This implies $\alpha_{i}+f_{i}^{\prime}(\boldsymbol{b}_{p})$ non-zero, and
moreover $v_{p}(\alpha_{i}+f_{i}^{\prime}(\boldsymbol{b}_{p}))\leq
v_{p}(\beta_{i}+g_{i}^{\prime}(\boldsymbol{b}_{p}))$ no matter what is the
value of $v_{p}(\beta_{i}+g_{i}^{\prime}(\boldsymbol{b}_{p}))$.

Note moreover that (IH1′:) and (IH2′:) directly imply
$\max\\{v_{p}(g(\boldsymbol{b}_{p}))\in\mathbb{N}:g\in\textup{terms}(\Psi^{\prime})\\}\leq
u$.

To conclude the proof, we show how to construct $\boldsymbol{b}_{p}$
satisfying (IH1′:) and (IH2′:).

base case $k=0$.

We establish (IH1′:) and (IH2′:) for polynomials with variables in
$\boldsymbol{x}$, by showing the three properties below, for every non-zero
polynomial $h\in\Delta(\Psi)$ with ${\textup{LV}(h)\preceq x_{d}}$.

  1. (A)

Either ${\mathbb{Z}f\cap\mathbb{Z}h\neq\\{0\\}}$ or $p\nmid
h(\boldsymbol{\nu}(\boldsymbol{x}))$.

  2. (B)

If $\mathbb{Z}f\cap\mathbb{Z}h\neq\\{0\\}$, then
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=v_{p}(f(\boldsymbol{\nu}(\boldsymbol{x})))$.

  3. (C)

If $p\nmid h(\boldsymbol{\nu}(\boldsymbol{x}))$ then
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=0$ and
$\mathbb{Z}h\cap\textup{M}_{f}(\Psi)=\\{0\\}$.

These three items imply (IH1′:) and (IH2′:). To establish (IH1′:), take
$g(\boldsymbol{x})\in\textup{terms}(\Psi)$ such that
$\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$. From (C) we must have
$p\mathrel{|}g(\boldsymbol{\nu}(\boldsymbol{x}))$. Hence,
${\mathbb{Z}f\cap\mathbb{Z}h\neq\\{0\\}}$ by (A), and from (B) we get
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=v_{p}(f(\boldsymbol{\nu}(\boldsymbol{x})))$.
For (IH2′:), take $h(\boldsymbol{x})\in\mathrm{S}_{f}(\Psi)$ such that
$\mathbb{Z}h\cap\textup{M}_{f}(\Psi)=\\{0\\}$. By definition of
$\textup{M}_{f}(\Psi)$, $\mathbb{Z}h\cap\mathbb{Z}f=\\{0\\}$ and so $p\nmid
h(\boldsymbol{\nu}(\boldsymbol{x}))$ by (A). From (C),
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=0$. We conclude the base case by
establishing (A)–(C).
Proof of (A): Since $\Psi$ has the elimination property,
$f\in\textup{terms}(\Psi)$. Then, (A) follows directly from (IH2:); remark
that $S(f,h)=0$ is equivalent to $\mathbb{Z}f\cap\mathbb{Z}h\neq\\{0\\}$.
Proof of (B): By $\mathbb{Z}f\cap\mathbb{Z}h\neq\\{0\\}$ there are
$\lambda_{1},\lambda_{2}\in\mathbb{Z}\setminus\\{0\\}$ such that
$\lambda_{1}\cdot f=\lambda_{2}\cdot h$. Without loss of generality,
$\gcd(\lambda_{1},\lambda_{2})=1$, and thus
$\gcd(\lambda_{2},\gcd(f))=\lambda_{2}$. The polynomial $f$ is primitive,
hence $\lambda_{2}=1$ and we get $h=\lambda_{1}\cdot f$. Since
$p\not\in\mathbf{P}_{\\!\\!+}(\Psi)$, from Condition (P2) and
$\lambda_{1}\mathrel{|}\gcd(h)$ we derive $p\nmid\lambda_{1}$. Therefore,
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=v_{p}(\lambda_{1}\cdot
f(\boldsymbol{\nu}(\boldsymbol{x})))=v_{p}(f(\boldsymbol{\nu}(\boldsymbol{x})))$.
Proof of (C): Trivially, $p\nmid h(\boldsymbol{\nu}(\boldsymbol{x}))$ equals
$v_{p}(h(\boldsymbol{\nu}(\boldsymbol{x})))=0$. To show
${\mathbb{Z}h\cap\textup{M}_{f}(\Psi)=\\{0\\}}$, first note that
$\mathbb{Z}h\cap\mathbb{Z}f=\\{0\\}$, directly from
$p\mathrel{|}f(\boldsymbol{\nu}(\boldsymbol{x}))$ and (B). _Ad absurdum_ ,
assume $\mathbb{Z}h\cap\textup{M}_{f}(\Psi)\not=\\{0\\}$. Since $\Psi$ is
increasing for
$\boldsymbol{\chi}\coloneqq(X_{1}\mathbin{\prec}\dots\mathbin{\prec}X_{r})$,
and $\textup{LV}(h)$ and $\textup{LV}(f)$ are both in $X_{1}$, $\Psi$ is
increasing no matter the order of the variables imposed on $X_{1}$. Take an
order $(\mathbin{\prec}^{\prime})\in\boldsymbol{\chi}$ for which
$\textup{LV}_{\mathbin{\prec}^{\prime}}(h)\,\preceq^{\prime}\,\textup{LV}_{\mathbin{\prec}^{\prime}}(f)$,
and let
${x_{1}^{\prime}\mathbin{\prec}^{\prime}\dots\mathbin{\prec}^{\prime}x_{d}^{\prime}}$
be the order for the variables $x_{1},\dots,x_{d}$. Since $\Psi$ is increasing
for $\mathbin{\prec}^{\prime}$,
$\textup{M}_{f}(\Psi)\cap\mathbb{Z}[x_{1}^{\prime},\dots,x_{\textup{LV}_{\mathbin{\prec}^{\prime}}(f)}^{\prime}]=\mathbb{Z}f$.
However,
$\mathbb{Z}h\subseteq\mathbb{Z}[x_{1}^{\prime},\dots,x_{\textup{LV}_{\mathbin{\prec}^{\prime}}(f)}^{\prime}]$
by definition of $\mathbin{\prec}^{\prime}$, hence from
$\mathbb{Z}h\cap\textup{M}_{f}(\Psi)\not=\\{0\\}$ we obtain
$\mathbb{Z}h\cap\mathbb{Z}f\not=\\{0\\}$, a contradiction. This proves (C).

induction step.

Let us assume that $b_{p,1},\dots,b_{p,k}$ are defined for the variables
$y_{1},\dots,y_{k}$ with $k\in[0,j-1]$, so that the induction hypotheses hold.
We provide the value $b_{p,k+1}$ for $y_{k+1}$ while keeping (IH1′:) and
(IH2′:) satisfied. We divide the proof into two cases, depending on whether
there is a term $g\in\textup{terms}(\Psi)$ with $\textup{LV}(g)=y_{k+1}$ such
that $\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$.

case $g$ does not exist.

In this case, (IH1′:) is fulfilled no matter the value of $b_{p,k+1}$, so we
focus on finding such a value satisfying (IH2′:). It suffices to consider the
system

$\displaystyle h(b_{p,1},\dots,b_{p,k},\,y_{k+1})$ $\displaystyle\not\equiv 0$
$\displaystyle\pmod{p}$ $\displaystyle h\in\mathrm{S}_{f}(\Psi)\text{
s.t.}~{}\textup{LV}(h)=y_{k+1}.$

Similarly to the system in Equation 13, writing $c_{h}+a_{h}\cdot y_{k+1}$ for
$h(b_{p,1},\dots,b_{p,k},\,y_{k+1})$, we obtain the equivalent system of non-
congruences

$\displaystyle y_{k+1}$ $\displaystyle\not\equiv-a_{h}^{-1}\cdot c_{h}$
$\displaystyle\pmod{p}$ $\displaystyle h\in\mathrm{S}_{f}(\Psi)\text{
s.t.}~{}\textup{LV}(h)=y_{k+1}.$

Since $p\not\in\mathbf{P}_{\\!\\!+}(\Psi)$ and from (P1), this system admits a
solution $b_{p,k+1}$ in $[0,p-1]$. Note that (IH2′:) is satisfied, since every
polynomial in that hypothesis is considered in these non-congruence systems.

case $g$ exists.

Recall that $g$ is a polynomial in $\textup{terms}(\Psi)$ such that
$\textup{LV}(g)=y_{k+1}$ and $\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$.
Let $u\coloneqq v_{p}(f(\boldsymbol{\nu}(\boldsymbol{x})))$. In order to
satisfy (IH1′:) it suffices to find $b_{p,k+1}\in\mathbb{Z}$ satisfying the
following (non-empty) system of non-congruences

$\displaystyle\forall g\in\textup{terms}(\Psi)\text{
s.t.}~{}\textup{LV}(g)=y_{k+1}\text{ and
}\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\},$
$\displaystyle\qquad\begin{aligned} g(b_{p,1},\dots,b_{p,k},\,y_{k+1})&\equiv
0&&\pmod{p^{u}}\\\ g(b_{p,1},\dots,b_{p,k},\,y_{k+1})&\not\equiv
0&&\pmod{p^{u+1}}.\end{aligned}$

Similarly to the system in Equation 13, writing $c_{g}+a_{g}\cdot y_{k+1}$ for
$g(b_{p,1},\dots,b_{p,k},\,y_{k+1})$, we obtain the equivalent system of non-
congruences

$\displaystyle\forall g\in\textup{terms}(\Psi)\text{
s.t.}~{}\textup{LV}(g)=y_{k+1}\text{ and
}\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\},$ (14)
$\displaystyle\qquad\begin{aligned} y_{k+1}&\equiv-a_{g}^{-1}\cdot
c_{g}&&\pmod{p^{u}}\\\ y_{k+1}&\not\equiv-a_{g}^{-1}\cdot
c_{g}&&\pmod{p^{u+1}}.\end{aligned}$

Focus on the congruences $y_{k+1}\equiv-a_{g}^{-1}\cdot c_{g}\pmod{p^{u}}$ of
this system. These only have a solution if the right-hand side is the same
modulo $p^{u}$ for every $g\in\textup{terms}(\Psi)$ with
$\textup{LV}(g)=y_{k+1}$ and $\mathbb{Z}g\cap\textup{M}_{f}(\Psi)\neq\\{0\\}$.
We prove that this is indeed the case. Consider $g_{1}$ and $g_{2}$ such that
$g_{i}\in\textup{terms}(\Psi)$ with $\textup{LV}(g_{i})=y_{k+1}$ and