English
In the TM1to1 construction, applying a write operation before moving the head yields the same next-step outcome as first moving the head and then continuing, when comparing the transformed tape with the original.
Русский
В конструции TM1to1 применение операции записи перед перемещением головки даёт тот же результат следующего шага, что и сначала перемещение головки, затем продолжение, при сопоставлении трансформированной ленты с исходной.
LaTeX
$$$\\operatorname{stepAux}\\bigl(\\operatorname{write}((\\operatorname{enc} a).toList)\\, q\\bigr)\\, v\\, \\operatorname{trTape}'(\\operatorname{enc0}, L, \\operatorname{ListBlank.cons}(b, R)) = \\operatorname{stepAux} q\\, v\\, \\operatorname{trTape}'(\\operatorname{enc0}, \\operatorname{ListBlank.cons}(a, L), R). $$$
Lean4
theorem stepAux_write (q : Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (a b : Γ) (L R : ListBlank Γ) :
stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
stepAux q v (trTape' enc0 (ListBlank.cons a L) R) :=
by
simp only [trTape', ListBlank.cons_flatMap]
suffices
∀ {L' R'} (l₁ l₂ l₂' : List Bool) (_ : l₂'.length = l₂.length),
stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
stepAux q v (Tape.mk' (L'.append (List.reverseAux l₂ l₁)) R')
by exact this [] _ _ ((enc b).2.trans (enc a).2.symm)
clear a b L R
intro L' R' l₁ l₂ l₂' e
induction l₂ generalizing l₁ l₂' with
| nil => cases List.length_eq_zero_iff.1 e; rfl
| cons a l₂
IH =>
rcases l₂' with - | ⟨b, l₂'⟩ <;> simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e
rw [List.reverseAux, ← IH (a :: l₁) l₂' e]
simp [stepAux, ListBlank.append, write]
