eval_pappAck — Mathlib

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₂]

Похожие утверждения