stepNormal_eval — Mathlib

English

Evaluating stepNormal c Cont.halt v yields the halt mapped to c.eval v; i.e., the machine halts with the same result as c on v.

Русский

Оценка stepNormal c Cont.halt v даёт halt на результат c.eval v.

LaTeX

$$$\\forall c\\,v.\\; eval\\ step\\ (stepNormal\\ c\\ Cont.halt\\ v) = \\operatorname{map}\\ (\\text{halt}) (c.eval\\ v)$$$

Lean4

theorem stepNormal_eval (c v) : eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v :=
  (code_is_ok c).zero

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