not_primrec_ack_self

Mathlib.Computability.Ackermann

URI: https://scilib.ai/kg/mathlib#not_primrec_ack_self

English

The function n ↦ ack(n,n) is not a primitive recursive function.

Русский

Функция n ↦ ack(n,n) не является примитивно рекурсивной.

LaTeX

$$$$\\neg\\ Primrec (\\lambda n.\\ ack(n,n)).$$$$

Lean4

theorem not_primrec_ack_self : ¬Primrec fun n => ack n n :=
  by
  rw [Primrec.nat_iff]
  exact not_nat_primrec_ack_self

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

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

Разделы

Аффилиация

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