English
For any f: Γ → Γ' (PointedMap) and any tapes T on Γ, moving the tape and then mapping f is the same as mapping f and then moving:
Русский
Для любого отображения f: Γ → Γ' (PointedMap) и любой ленты T над Γ перемещение ленты и отображение f commute: отображение f после перемещения равно перемещению после отображения.
LaTeX
$$$ \forall {\Gamma} {\Gamma'} [\mathrm{Inhabited } {\Gamma}] [\mathrm{Inhabited } {\Gamma'}] (f: \text{PointedMap } {\Gamma} {\Gamma'}) (T: \text{Tape } {\Gamma}) (d),\ (T.move\ d).map f = (T.map f).move\ d $$$
Lean4
theorem map_move {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (T : Tape Γ) (d) :
(T.move d).map f = (T.map f).move d := by
cases T
cases d <;> simp only [Tape.move, Tape.map, ListBlank.head_map, ListBlank.map_cons, ListBlank.tail_map]
