Background
By the MRDP theorem, every for every recursively enumerable set $S$, there exists a Diophantine polynomial $p$ such that
$$x \in S \iff \exists y_1, \dots, y_n \in \mathbb{N} \text{ such that } p(x \, | \, y_1, \dots, y_n) = 0$$
Adelman & Manders define the complexity class $D$ as those r.e. sets with a Diophantine expression whose inputs have polynomial-bounded length; that is, for some polynomial $b$,
$$x \in S \in D \iff \exists y_1, \dots, y_n \le 2^{b(|x|)} \text{ such that } p(x \, | \, y_1, \dots, y_n) = 0$$
Adelman & Manders conjecture that $D = NP$, and show a few "$D$-Complete" problems - for example, the regular language $R_0 = (10 + 00)^*$ is in $D$ iff $D = NP$.
One might ask - if we use some sort of logical encoding of $R_0$, which logical construct do we not know how to encode in Diophantine language without pushing the problem out of $D$? The answer seems to be polynomial-bounded universal quantifiers: the encoding of $R_0$ looks something like
$$\forall i \le \frac{|x|}{2} \text{ (x[2i] = 0)}$$
And the predicate $x[2i] = 0$ is in $D$ for any single choice of $i$, but we leave $D$ when we use the current best encoding methods to turn the bounded $\forall$ term into a series of $\exists$ terms attached to a more complex polynomial.
Questions
Is my intuition correct that there is no obvious track for proving $D=NP$ besides a successful coding scheme for the quantifiers?
(second question deleted; answered in comments)