Cook and Nguyen, Logical Foundations of Proof Complexity, on p. 42, ask for a proof in $I \Delta_0$ of $\exists z(x + z = y \lor y + z = x)$, and give as hint, "Induction on $x$. Base case: B2, O2. Induction step: B3, B4, D1."
The obvious induction predicate is $\phi(x)$ as $\exists z(x + z = y \lor y + z = x)$, only the quantifier isn't bounded. So it seems one needs to prove: $\exists z≤y(x + z = y) \lor \exists z≤ x(y + z = x)$. But, trying to prove this, I would like to use transitivity of $≤$ at some point. But transitivity is proved later, as D4, and the hints of the proof of D4 rely on D3, which rely on D2.
Am I missing something simple, or worse am I misunderstanding something simple?
D3 is $x ≤ y \iff \exists z(x + z =y)$
