eval_pappAck_step_succ — Mathlib

English

For any c and n, (pappAck.step c).eval (n+1) equals ((pappAck.step c).eval n).bind c.eval.

Русский

Для любых c и n: (pappAck.step c).eval(n+1) = ((pappAck.step c).eval n) .bind c.eval.

LaTeX

$$$$\\forall c\\, \\forall n, \\ (pappAck\\.step c).\\eval \$n+1\$ = \\big(((pappAck\\.step c)\\.\\eval n) \\).\\bind\\ c.\\eval.$$$$

Lean4

@[simp]
theorem eval_pappAck_step_succ (c : Code) (n) : (pappAck.step c).eval (n + 1) = ((pappAck.step c).eval n).bind c.eval :=
  by simp [pappAck.step, Code.eval]

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