English
Similar to the previous exists_code, there exists a code implementing the composition of two partially computable codes when given their respective realizations.
Русский
Похожий на предыдущее exists_code факт: существует код, реализующий композицию двух частично вычислимых кодов при их реализациях.
LaTeX
$$$\\exists c\\, \\forall v. c.eval(v) = \\operatorname{pure}\\big((\\mathrm{List}.Vector.mOfFn(\\lambda i. g i\\ v)) \\bind f\\big)$$$
Lean4
/-- The `stepNormal` function respects the `then k'` homomorphism. Note that this is an exact
equality, not a simulation; the original and embedded machines move in lock-step until the
embedded machine reaches the halt state. -/
theorem stepNormal_then (c) (k k' : Cont) (v) : stepNormal c (k.then k') v = (stepNormal c k v).then k' := by
induction c generalizing k v with simp only [stepNormal, *]
| cons c c' ih _ => rw [← ih, Cont.then]
| comp c c' _ ih' => rw [← ih', Cont.then]
| case => cases v.headI <;> simp only [Nat.rec_zero]
| fix c ih => rw [← ih, Cont.then]
| _ => simp only [Cfg.then]
