English
A technical lemma describing how Respects lifts through a run of the emulator, establishing reachability preservation through intermediate steps.
Русский
Техническая лемма, описывающая как свойство сохранения относится к последовательности выполнения эмулятора, устанавливая сохранение достижимости на промежуточных шагах.
LaTeX
$$$ \forall k, H:\; Reaches₀ (TM1.step (tr M)) \; \langle \dots \rangle \Rightarrow \dots $$$
Lean4
theorem tr_respects_aux₁ {k} (o q v) {S : List (Γ k)} {L : ListBlank (∀ k, Option (Γ k))}
(hL : L.map (proj k) = ListBlank.mk (S.map some).reverse) (n) (H : n ≤ S.length) :
Reaches₀ (TM1.step (tr M)) ⟨some (go k o q), v, Tape.mk' ∅ (addBottom L)⟩
⟨some (go k o q), v, (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))⟩ :=
by
induction n with
| zero => rfl
| succ n IH =>
apply (IH (le_of_lt H)).tail
rw [iterate_succ_apply']
simp only [TM1.step, TM1.stepAux, tr, Tape.mk'_nth_nat, Tape.move_right_n_head, addBottom_nth_snd, Option.mem_def]
rw [stk_nth_val _ hL, List.getElem?_eq_getElem]
· rfl
· rwa [List.length_reverse]
