English
A counterpart of a step-wise respect lemma focusing on a fixed base configuration and advancing through moves.
Русский
Соответствующая по шагам версия леммы о сохранении свойств через базовую конфигурацию и перемещения.
LaTeX
$$$ \forall n, \dots \Rightarrow Reaches₀( TM1.step( tr M)) \dots$$$
Lean4
theorem tr_respects_aux₃ {q v} {L : ListBlank (∀ k, Option (Γ k))} (n) :
Reaches₀ (TM1.step (tr M)) ⟨some (ret q), v, (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))⟩
⟨some (ret q), v, Tape.mk' ∅ (addBottom L)⟩ :=
by
induction n with
| zero => rfl
| succ n IH =>
refine Reaches₀.head ?_ IH
simp only [Option.mem_def, TM1.step]
rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst, TM1.stepAux,
iterate_succ', Function.comp_apply, Tape.move_right_left]
rfl
