English
If f is Code.Ok, then evaluating the fixed continuation f.fix on input v under step yields the same result as first evaluating f.fix and then feeding to the ret code.
Русский
Если f является Code.Ok, то при вычислении фиксации континуума f.fix на входе v в шаге получаем тот же результат, что и при первом вычислении f.fix, затем передаче результата в код возврата.
LaTeX
$$$\\text{cont\_eval\_fix: }\\ (fok)\\;\\Rightarrow\\; Turing.eval step (stepNormal f (Cont.fix f k) v) = f.fix.eval v \\gg= (\\\\lambda v. Turing.eval step (Cfg.ret k v))$$$
Lean4
theorem zero {c} (h : Code.Ok c) {v} : Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> Code.eval c v :=
by
rw [h, ← bind_pure_comp]; congr; funext v
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)
