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.