ack_succ_zero

Mathlib.Computability.Ackermann

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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