English
Let f: Γ → Γ, L,R : ListBlank Γ, and n ∈ ℕ. Writing f(R.nth n) after performing n right-moves on Tape.mk' L R yields the tape obtained by applying n right-moves to Tape.mk' L (R.modifyNth f n).
Русский
Пусть f: Γ → Γ, L,R : ListBlank Γ и n ∈ ℕ. Запись f(R.nth n) после выполнения n правых сдвигов на Tape.mk' L R даёт ленту, полученную после n правых сдвигов на Tape.mk' L (R.modifyNth f n).
LaTeX
$$$ \forall {\Gamma} [\text{Inhabited } {\Gamma}] (f : {\Gamma} \to {\Gamma}) (L R : \text{ListBlank } {\Gamma}) (n : \mathbb{N}),\\ (Tape.write (f (R.nth n)) ( (\mathrm{Tape.move}\ {}^{n}) (\mathrm{Tape.mk'} L R) )) = ( (\mathrm{Tape.move}\ {}^{n}) (\mathrm{Tape.mk'} L (R.modifyNth f n)) ) $$$
Lean4
@[simp]
theorem write_move_right_n {Γ} [Inhabited Γ] (f : Γ → Γ) (L R : ListBlank Γ) (n : ℕ) :
((Tape.move Dir.right)^[n] (Tape.mk' L R)).write (f (R.nth n)) =
(Tape.move Dir.right)^[n] (Tape.mk' L (R.modifyNth f n)) :=
by
induction n generalizing L R with
| zero =>
simp only [ListBlank.nth_zero, ListBlank.modifyNth, iterate_zero_apply]
rw [← Tape.write_mk', ListBlank.cons_head_tail]
| succ n IH =>
simp only [ListBlank.head_cons, ListBlank.nth_succ, ListBlank.modifyNth, Tape.move_right_mk', ListBlank.tail_cons,
iterate_succ_apply, IH]
