computable₂_ack — Mathlib

English

The Ackermann function is computable (in the sense of two-argument computability).

Русский

Функция Аккермана вычислима (в смысле двух аргументов).

LaTeX

$$$$\\operatorname{Computable}_2\\ ack.$$$$

Lean4

/-- The Ackermann function is computable. -/
theorem _root_.computable₂_ack : Computable₂ ack :=
  by
  apply _root_.Partrec.of_eq_tot (f := fun p : ℕ × ℕ => (pappAck p.1).eval p.2) (g := fun p : ℕ × ℕ => ack p.1 p.2)
  · change Partrec₂ (fun m n => (pappAck m).eval n)
    apply_rules only [Code.eval_part.comp₂, Computable.fst, Computable.snd, primrec_pappAck.to_comp.comp]
  · simp

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