English
For any k, q, S, v and a StAct s, stepping the emulated TM2 with stRun equals the TM2 step with updated state.
Русский
Для любых k, q, S, v и действие StAct s переход эмулятора TM2 через stRun эквивалентен шагу TM2 с обновлённым состоянием.
LaTeX
$$$ \forall k, q, S, v, s:\; TM2.stepAux (stRun s q) v S = TM2.stepAux q (stVar v (S k) s) (update S k (stWrite v (S k) s)) $$$
Lean4
theorem step_run {k : K} (q : TM2.Stmt Γ Λ σ) (v : σ) (S : ∀ k, List (Γ k)) :
∀ s : StAct K Γ σ k, TM2.stepAux (stRun s q) v S = TM2.stepAux q (stVar v (S k) s) (update S k (stWrite v (S k) s))
| StAct.push _ => rfl
| StAct.peek f => by unfold stWrite; rw [Function.update_eq_self]; rfl
| StAct.pop _ => rfl
