A proof of Bel'tyukov - Lipshitz theorem by quasi-quantifier elimination. II. The main reduction

This paper is the second part of a new proof of the Bel'tyukov - Lipshitz theorem, which states that the existential theory of the structure $\langle\mathrm{Z}; 0, 1, +, -, \leqslant ,|\rangle$ is decidable. We construct a quasi-quantifier elimination algorithm (the notion was introduced in the first part of the proof) to reduce the decision problem for the existential theory of $\langle\mathrm{Z}; 0, 1, +, -, \leqslant ,GCD\rangle$ to the decision problem for the positive existential theory of the structure $\langle\mathrm{Z}_{>0}; 1 \{a\cdot\}_{a\in\mathrm{Z}_{>0}} , GCD\rangle$ . Since the latter theory was proved decidable in the first part, this reduction completes the proof of the theorem. Analogues of two lemmas of Lipshitz's proof are used in the step of variable isolation for quasi-elimination. In the quasi-elimination step we apply GCD-Lemma, which was proved in the first part.