not_primrec₂_ack

Mathlib.Computability.Ackermann

URI: https://scilib.ai/kg/mathlib#not_primrec₂_ack

← MathLib Explorer

English

The two-argument Ackermann function is not primitive recursive.

Русский

Функция Аккермана с двумя аргументами не является примитивно рекурсивной.

LaTeX

$$$$\\neg\\ Primrec_2 \\ ack.$$$$

Lean4

/-- The Ackermann function is not primitive recursive. -/
theorem not_primrec₂_ack : ¬Primrec₂ ack := fun h => not_primrec_ack_self <| h.comp Primrec.id Primrec.id

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

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

Разделы

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

Аффилиация

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