Prove that for any quantifier-free sentence $\tau$ true in $\mathcal{N}$, $A_E \vdash \tau$. We define $\mathcal{N}$ to be $\langle \mathbb{N}, 0,S,+,\cdot, E, <\rangle$ (where $E$ is a binary exponent function) and $T_E$ is the theory of the arithmetic axioms $A_E$.
Here's what I've tried: for terms $t_1$ and $t_2$, we need to prove $t_1 = t_2$ from $A_E$ and next $t_1 < t_2$ from $A_E$. In the first case we must differentiate between $S^n (0)$ (the $n$th successor of $0$) and the number $n$. To do so, we must show $n = m$ iff $S^n(0) = S^m(0)$ which is pretty trivial I think. Then we must show $n < m$ iff $S^n(0) < S^m(0)$ which I'm not sure how to show other than using this lemma that tells us we can prove from $A_E$ $\forall x (x < S^{k+1}(0) \leftrightarrow x = S^0 (0) \lor \cdots \lor x = S^k(0))$.
After establishing these facts, we can see that there is a proof from $A_E$ of $t_1=S^m(0)$ for some $m$ and $t_2 = S^n(0)$ for some $n$ (don't need to prove this for my purposes). Then the $t_1 = t_2$ case follows pretty directly and the $t_1<t_2$ case contains 6 steps.
Am I on the right track and is there anything I'm missing?