English
A compatibility result: stepping TM0 configuration corresponds to stepping TM1 configuration after transformation.
Русский
Совместимость переходов: переход конфигурации TM00 соответствует переходу конфигурации TM1 после преобразования.
LaTeX
$$$$\\operatorname{tr\\_respects}: \\operatorname{Respects}(\\operatorname{TM0.step} M, \\operatorname{TM1.step}(\\operatorname{tr} M)) \\; (a,b) \\Rightarrow \\; \\operatorname{trCfg}(M,a) = b.$$$$
Lean4
theorem tr_respects : Respects (TM0.step M) (TM1.step (tr M)) fun a b ↦ trCfg M a = b :=
fun_respects.2 fun ⟨q, T⟩ ↦ by
rcases e : M q T.1 with - | val
· simp only [TM0.step, trCfg, e]; exact Eq.refl none
obtain ⟨q', s⟩ := val
simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some]
revert e
have :
TM1.step (tr M) ⟨some (Λ'.act s q'), (), T⟩ =
some
⟨some (Λ'.normal q'), (),
match s with
| TM0.Stmt.move d => T.move d
| TM0.Stmt.write a => T.write a⟩ :=
by cases s <;> rfl
intro e
refine TransGen.head ?_ (TransGen.head' this ?_)
· simp only [TM1.step, TM1.stepAux, tr]
rw [e]
rfl
cases e' : M q' _
· apply ReflTransGen.single
simp only [TM1.step, TM1.stepAux, tr]
rw [e']
rfl
· rfl