primrec_pappAck_step

Mathlib.Computability.Ackermann

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

← MathLib Explorer

English

The function pappAck.step is primitive recursive.

Русский

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

LaTeX

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

Lean4

theorem primrec_pappAck_step : Primrec pappAck.step := by
  apply_rules [Code.primrec₂_curry.comp, Code.primrec₂_prec.comp, Code.primrec₂_comp.comp, _root_.Primrec.id,
    Primrec.const]

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

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

Разделы

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

Аффилиация

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