primrec_pappAck

Mathlib.Computability.Ackermann

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.primrec_pappAck

← MathLib Explorer

English

The function pappAck is primitive recursive.

Русский

Функция pappAck примитивно рекурсивна.

LaTeX

$$$$\\operatorname{Primrec}\\ (pappAck).$$$$

Lean4

theorem primrec_pappAck : Primrec pappAck :=
  by
  suffices Primrec (Nat.rec Code.succ (fun _ c => pappAck.step c)) by convert this using 2 with n;
    induction n <;> simp [pappAck, *]
  apply_rules [Primrec.nat_rec₁, primrec_pappAck_step.comp, Primrec.snd]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru