Существование неэффективизируемых оценок в теории экспоненциально диофантовых уравнений

Примером оценок, упоминаемых в названии, служит приводимое ниже следствие основной теоремы:
Можно построить полином $A(a,x_1,\dots,x_{\nu})$ с целыми коэффициентами, удовлетворяющий следующим условиям. Во-первых, для любого натурального $a$ уравнение $A(a,x_1,\dots,x_{\nu},y+4^y)$ не имеет более одного решения в натуральных $x_1,\dots,x_{\nu},y$. Во-вторых, для любой общерекурсивной (вычислимой) функции $C$ найдется значение $a$, для которого существует решение $x_1,\dots,x_{\nu},y$ приведенного выше уравнения, такое что
$$ \max\{x_1,\dots,x_{\nu},y\}>C(a). $$
Основная теорема утверждает, что для любого рекурсивно перечислимого предиката $P(a_1,\dots,a_{\lambda})$ имеются выражения $\mathfrak A$ и $\mathfrak L$, построенные из натуральных чисел и переменных $a_1,\dots,a_{\lambda}$, $z_1,\dots,z_{\chi}$ с помощью сложения, умножения и возведения в степень, такие что
$$ P(a_1,\dots,a_{\lambda})\Leftrightarrow(\exists z_1\dotsb z_{\chi})[\mathfrak A=\mathfrak L_1]\Leftrightarrow(\exists!z_1\dotsb z_{\chi})[\mathfrak A=\mathfrak L_1]. $$
Обсуждается возможность получения аналогичных результатов для диофантовых уравнений.