ack_succ_succ

Mathlib.Computability.Ackermann

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

English

For all m,n, A(m+1,n+1) = A(m, A(m+1,n)).

Русский

Для всех m,n: A(m+1,n+1) = A(m, A(m+1,n)).

LaTeX

$$$$\operatorname{ack}(m+1,n+1) = \operatorname{ack}(m, \operatorname{ack}(m+1,n)).$$$$

Lean4

@[simp]
theorem ack_succ_succ (m n : ℕ) : ack (m + 1) (n + 1) = ack m (ack (m + 1) n) := by rw [ack]

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

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

Разделы

Аффилиация

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