eval_pappAck_step_zero

Mathlib.Computability.Ackermann

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

English

For any code c, evaluating pappAck.step c at 0 equals evaluating c at 1.

Русский

Для любого кода c значение (pappAck.step c).eval(0) равно c.eval(1).

LaTeX

$$$$\\forall c, \\ (pappAck\\.step c).\\eval\\ 0 = c.\\eval\\ 1.$$$$

Lean4

@[simp]
theorem eval_pappAck_step_zero (c : Code) : (pappAck.step c).eval 0 = c.eval 1 := by simp [pappAck.step, Code.eval]

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

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

Разделы

Аффилиация

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