English
If a,b ∈ Γ and L,R are ListBlank Γ, then (Tape.mk' L R).write b = Tape.mk' L (R.cons b) and more generally, writing to a tape built with Mk' updates only the head value.
Русский
Если a, b ∈ Γ и L, R — ListBlank Γ, то (Tape.mk' L R).write b = Tape.mk' L (R.cons b) и в общем случае запись в ленте, построенной Mk', обновляет только голову.
LaTeX
$$$ \forall {\Gamma} [\text{Inhabited } {\Gamma}] (a b : {\Gamma}) (L R : \text{ListBlank } {\Gamma}),\ (Tape.mk' L (R.cons a)).write b = Tape.mk' L (R.cons b) $$$
Lean4
@[simp]
theorem write_mk' {Γ} [Inhabited Γ] (a b : Γ) (L R : ListBlank Γ) :
(Tape.mk' L (R.cons a)).write b = Tape.mk' L (R.cons b) := by
simp only [Tape.write, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons]
