Доказательство теоремы Бельтюкова - Липшица квазиэлиминацией кванторов. II. Основное сведение

Работа является второй частью нового доказательства теоремы Бельтюкова-Липшица о разрешимости экзистенциальной теории структуры $\langle\mathrm{Z}; 0, 1, +, -, \leqslant ,|\rangle$. Строится алгоритм квази-ЭК (понятие введено в первой части доказательства), осуществляющий сведение проблемы разрешимости для экзистенциальной теории структуры $\langle\mathrm{Z}; 0, 1, +, -, \leqslant, $ НОД$\rangle$ к проблеме разрешимости для позитивной экзистенциальной теории структуры $\langle\mathrm{Z}_{>0}; 1 \{a\cdot\}_{a\in\mathrm{Z}_{>0}} ,$ НОД$\rangle$. Так как разрешимость последней теории была доказана в первой части, построенное сведение завершит доказательство теоремы. На шаге отделения переменной для квазиэлиминации используются аналоги двух лемм из доказательства Липшица. Шаг квазиэлиминации основан на НОДлемме, доказанной в первой части.