English
The transformed and original stepping relations are compatible: stepping the original machine and stepping the transformed machine correspond to the same observable configuration, up to the encoding trCfg.
Русский
Переходы в преобразованной и исходной моделях совместимы: пошаговое выполнение исходной машины и пошаговое выполнение преобразованной машины соответствуют одной и той же наблюдаемой конфигурации посредством кодирования trCfg.
LaTeX
$$$$\\operatorname{Respects}(\\operatorname{step} M, \\operatorname{step}(\\operatorname{tr} enc dec M))\\; (c_1, c_2)\\;\\Rightarrow\\; \\operatorname{trCfg}(enc, enc0)(c_1) = c_2.$$$$
Lean4
theorem tr_respects : Respects (step M) (step (tr enc dec M)) fun c₁ c₂ ↦ trCfg enc enc0 c₁ = c₂ :=
fun_respects.2 fun ⟨l₁, v, T⟩ ↦ by
obtain ⟨L, R, rfl⟩ := T.exists_mk'
rcases l₁ with - | l₁
· exact rfl
suffices
∀ q R,
Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
(trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
by
refine TransGen.head' rfl ?_
rw [trTape_mk']
exact this _ R
clear R l₁
intro q R
induction q generalizing v L R with
| move d q IH =>
cases d <;>
simp only [trNormal, stepAux_move, stepAux, Tape.move_left_mk', trTape'_move_left enc0,
trTape'_move_right enc0] <;>
apply IH
| write f q IH =>
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
refine ReflTransGen.head rfl ?_
obtain ⟨a, R, rfl⟩ := R.exists_cons
rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move, trTape'_move_left enc0,
ListBlank.head_cons, ListBlank.tail_cons, Tape.write_mk']
apply IH
| load a q IH =>
simp only [trNormal, stepAux_read dec enc0 encdec]
apply IH
| branch p q₁ q₂ IH₁
IH₂ =>
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
grind
| goto l =>
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
apply ReflTransGen.refl
| halt =>
simp only [trNormal, stepAux, trCfg, trTape_mk']
apply ReflTransGen.refl
