Do you know if I can find the proof that the existential theory of $\mathbb{Z}$ with the structure of addition , divisibility and the relation $(\exists s \in \mathbb{Z})m=np^s$ is undecidable, besides the one of the paper of J. Denef "The diophantine problem for polynomial rings of positive characteristic" ?

Do you know if I can find the proof that the existential theory of $\mathbb{Z}$ with the structure of addition , divisibility and the relation $(\exists s \in \mathbb{Z})m=np^s$ is undecidable, besides the one of the paper of J. Denef "The diophantine problem for polynomial rings of positive characteristic" ?

In the paper of Denef, the corollary is stated as followed:

Let $p$ be a fixed prime number, $p>1$.

Define the relation $|^p$ by $$x |^p y \leftrightarrow \exists f \in \mathbb{N} : y= \pm x p^f$$

Then the positive existential theory of $(\mathbb{Z}; +, | , |^p)$ is undecidable.