Quantifier elimination of $\exists x\bigwedge \Delta$

Question

I'm currently studying logic and theory of computation (right now I'm concerned with quantifier elimination). Consider the successor theory generated by the following axioms $$(S1)\,\forall\, x\neg S(x)=0;$$ $$(S2)\,\forall x\forall y\,(S(x)=S(y)\rightarrow x=y);$$ $$(S3)\,\forall x\,((\neg x=0)\rightarrow \exists y\,S(y)=x);$$ $$(S4)\,\forall x\,\neg S^k(x)=x.$$ Say there is a set $\Delta$ with elements of the form $$S^n(x)=S^m(y),$$ where $0<n<m.$ My goal is to eliminate the quantifiers of $\exists x\bigwedge \Delta$, but I can't find a method that solves this. Any help? Thanks in advance

Answer 1

Given $0 < n < m$, $S^n(x) = S^m(y)$ is equivalent to $x = S^{m-n}(y)$ (by using $S2$ $n$ times). But then $\exists x \phi$, where $\phi$ is a conjunction including the formula $S^n(x) = S^m(y)$ is equivalent to $\phi[S^{m-n}(y)/x]$ (the resulting of substituting $S^{m-n}(y)$ for each occurrence of $x$ in $\phi$).