I am studying a paper written by Jan Denef on The rationality of the Poincaré series associated to the $p$-adic points on a variety. In this paper he defines an integral over a set $$D= \{(x,w)\in\mathbb{Z}_p^m\times \mathbb{Z}_p\mid \exists y\in\mathbb{Z}_p^m:x\equiv y\mod w,\text{ and }f_i(y)=0,\text{ for }i=1,\ldots,r\}$$ with $f_i\in\mathbb{Z}_p[x_1,\ldots,x_m]$.
In the paper he claims we can use Macintyre's theorem on the elimination of quantifiers, which says for $S$ a boolean combination of subsets of $\mathbb{Q}_p^{m+q}$ of type III, the set $$\{x\in\mathbb{Q}_p^m\mid\exists y\in\mathbb{Q}_p^q:(x,y)\in S\}$$ is a boolean combination of subsets of $\mathbb{Q}_p^m$ of type III.
A boolean combination of subsets of $\mathbb{Q}_p^m$ of type III is a subset created by unions, intersections and taking complements finitely many times of subsets of $\mathbb{Q}_p^m$ of type III.
A subset of type I is of the form $$\{x\in\mathbb{Q}_p^m\mid f(x)=0\}$$ $f\in\mathbb{Z}_p[x_1,\ldots,x_m]$. A subset of type II is of the form $$\{x\in\mathbb{Q}_p^m\mid\operatorname{ord}(f(x))\geq\operatorname{ord}(g(x))\}$$ $f,g\in\mathbb{Z}_p[x_1,\ldots,x_m]$. A subset of type III is of the form $$\{x\in\mathbb{Q}^m_p\mid\exists y\in\mathbb{Q}_p:f(x)=y^n\}$$ for $n\in\mathbb{N}, n\geq 2$, and $f\in\mathbb{Z}_p[x_1,\ldots,x_m]$.
He proves in the paper that subsets of type I and II are also of type III.
To use Macintyre's theorem, we need to write $D$ in the form used in the theorem. So we need to find a proper boolean combination $S$.
Now the condition that $f_i(y) = 0$ we can just use the sets $$\{(x,w,y)\in\mathbb{Q}_p^m\times\mathbb{Q}_p\times\mathbb{Q}_p^m\mid \tilde{f}_i(x,w,y)=0\}$$ where $\tilde{f}_i(x,w,y) = f_i(y)$. But I am a bit stuck on trying to translate the condition $x\equiv y\mod w$ into a boolean combination of these types.
Edit: I have come up with a way to do this by taking an infinite amount of sets. Let us put an order on the $m$-tuples over $\mathbb{Z}$ and denote these by $k_i$. Then the set $\{(x,w,y)\mid x\equiv y\mod w\}$ can be written as $$\bigcup_{i\in\mathbb{Z}}\{(x,w,y)\mid x-y-k_iw=0\}$$ Of course this is an infinite union so it is not a boolean combination.
Does anyone know a way to write it as a boolean combination? It must be possible since I guess otherwise the proof by Denef is false.
Second edit: If we suppose $\operatorname{ord}(w)=n$, we get that $(x,w)\in D$ if and only if $(x,p^n)\in D$. Perhaps this can be of some help? I only see how this is useful when infinite unions are also allowed.
The basic fact I was missing was this: If $x,y\in\mathbb{Q}_p$, we get $x\equiv y \mod w\iff \operatorname{ord}(x-y)\geq \operatorname{ord}(w)$. Indeed, if $x-y$ is a multiple of $w$, then $x-y$ is divisible by $p$ at least as many times as $w$ is. Conversely, if $\operatorname{ord}(x-y)\geq \operatorname{ord}(w)$. Write $w = ap^n+bp^{n+1}+\cdots, x-y=cp^m+dp^{m+1}+\cdots$, with $m\geq n$. We can see by the long division algorithm that $(x-y)/w$ is of the form $x_{n-m}p^{n-m}+\cdots\in\mathbb{Z}_p$.
Now for $x,y\in\mathbb{Q}_p^m$, we can apply this fact on the components. $$S_i = \{(x,w,y)\in\mathbb{Q}_p^m\times\mathbb{Q}_p\times\mathbb{Q}_p^m\mid \operatorname{ord}(x_i-y_i) \geq \operatorname{ord}(w)\}$$ Then the intersection of these $S_i$'s for $i=1,\ldots,m$ are the elements which satisfy $x\equiv y\mod w$.