A transfer method from bounded existential Diophantine equations to Tarski algebra formulas

We identify a transfer method from bounded existentially quantified Diophantine equations to formulas of Tarski algebra, the first order theory of the real field. The method is applied to show that NP is contained in ⋃n=1∞Dtime(2a⋅logO(1)n), where a depends only on the given Diophantine equation.