О разрешимости расширенных теорий сложения натуральных и целых чисел

Доказывается разрешимость элементарных теорий сложения натуральных и целых чисел в сигнатуре, расширенной одноместным предикатом, выделяющим степени фиксированного простого числа $p$, и двухместным предикатом $x|_{Pr}y$, выделяющим такие $x$ и $y$, что $x$ – степень $p$, и $x$ делит натуральное число $y$.
Библ. 5.