English
For all m,n, (pappAck m).eval n = some (ack m n).
Русский
Для всех m,n: (pappAck m).eval n = some (ack m n).
LaTeX
$$$$\\forall m,n, \\ (pappAck \\; m).\\eval \\; n = \\operatorname{Part}.\\some (\\operatorname{ack}(m,n)).$$$$
Lean4
@[simp]
theorem eval_pappAck (m n) : (pappAck m).eval n = Part.some (ack m n) := by
induction m, n using ack.induct with
| case1 n => simp [Code.eval, pappAck]
| case2 m hm => simp [pappAck, hm]
| case3 m n hmn₁ hmn₂ => dsimp only [pappAck] at *; simp [hmn₁, hmn₂]