unrev_ok — Mathlib

English

There is a valid run for the unrev operation translated into TM2, updating the stack to reflect reversal correctly.

Русский

Существует корректный переход вычисления для операции unrev, переведённой в TM2, соответственно обновляющей стек.

LaTeX

$$$\\text{unrev\\_ok} \\;: \\; \\text{Reaches}_1 (\\text{TM2.step} \\; tr) \\;\\langle\\dots,\\;\\operatorname{unrev}(q)\\rangle \\Rightarrow \\text{…}$$$

Lean4

theorem unrev_ok {q s} {S : K' → List Γ'} :
    Reaches₁ (TM2.step tr) ⟨some (unrev q), s, S⟩
      ⟨some q, none, update (update S rev []) main (List.reverseAux (S rev) (S main))⟩ :=
  move_ok (by decide) <| splitAtPred_false _

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