English
stepRet (k.then k') v equals (stepRet k v).then k'.
Русский
stepRet (k.then k') v равно (stepRet k v).then k'.
LaTeX
$$$\\operatorname{stepRet}\\ (k.\\text{then}\\ k')\\ v = (\\operatorname{stepRet}\\ k\\ v).\\text{then}\\ k'$$$
Lean4
/-- The `stepRet` 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 stepRet_then {k k' : Cont} {v} : stepRet (k.then k') v = (stepRet k v).then k' := by
induction k generalizing v with simp only [Cont.then, stepRet, *]
| cons₁ =>
rw [← stepNormal_then]
rfl
| comp => rw [← stepNormal_then]
| fix _ _ k_ih =>
split_ifs
· rw [← k_ih]
· rw [← stepNormal_then]
rfl
| _ => simp only [Cfg.then]
