I am trying to understand the proof of the aforementioned fact. For context, here's a rough outline of [what I am understanding to be] the idea behind the proof: in the language we construct a formula $\phi(x)$ asserting "machine $x$, when started on input $x$, halts in less than $f(|x|)$ steps", where $f:x\mapsto 2^{2^{kx}}$ for some $k$. Next, given any machine $M$ intending to decide $PrA$, we construct a machine $M'$ as follows: when started on input $w$, $M'$ overwrites it with $\neg\phi(w)$, then runs $M$ to decide it. If $M$ decides $\neg\phi(w) \in PrA$, $M'$ halts, otherwise it loops forever. The conclusion is that any machine that decides $PrA$ must take $\geq f(|\sharp M'|)$ steps to decide $\neg\phi(\sharp M')$ - otherwise we get a contradiction when we run $M'$ on $\sharp M'$. So far so good, I guess.
I get lost when it is time to construct $\phi$, though. For example, one of the building blocks [used in the construction] of $\phi$ is a formula $I_{n}(x)$, $|I_{n}(x)| = O(n)$, asserting "$x$ is less than $f(n)^{2}$". Now, the paper doesn't show how to construct this formula, and I have no idea how to, too, given that we can only use addition and we have that bound there.
What am I missing?
EDIT, as suggested: the proof I am talking about is in Rabin and Fischer's paper - .pdf available here.1 And one further thing: I found one post from Lipton's blog where he talks about the "trick" used to construct $I_{n}$ succinctly. It is a sketch only and unfortunately not enough for me. It is mentioned however that the trick was previously discovered by Fischer and Meyer, and Volker Strassen, independently, but I couldn't track down these papers describing it in detail - if anyone knows about them, please tell me!
1Michael J. Fischer, Michael O. Rabin: Super-exponential complexity of Presburger arithmetic. Also: CiteSeerX, MIT, DOI: 10.1007/978-3-7091-9459-1_5, http://hcs64.com/files/cc.pdf#page=35
Fischer and Rabin don't explicitly construct $_()$. Instead they claim its existence is clear in the proof of Theorem 11. This is essentially true, since the multiplication formula $M_n(x,y,z)$ they construct in the proof of Theorem 8 satisfies $M_n(x,y,z) \leftrightarrow x < 2^{2^n} ∧ x·y = z ∧ x ∈ N.$
This fact can be used to define $_()$. Namely, set $_() = M_{n+1}(x,0,0)$ for x ∈ N. Since x·0 = 0 and x ∈ N, $M_{n+1}(x,0,0) \leftrightarrow x < 2^{2^{n+1}} = (2^{2^n})^2$