move_left_mk' — Mathlib

English

Moving left on Tape.mk' L R yields Tape.mk' L.tail (R.cons L.head).

Русский

Перемещение влево относительно Tape.mk' L R дает Tape.mk' L.tail (R.cons L.head).

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)] (L R : ListBlank(\Gamma)), (Tape.move\ Dir.left\ (Tape.mk' L R)) = Tape.mk' L.tail (R.cons L.head)$$$

Lean4

@[simp]
theorem move_left_mk' {Γ} [Inhabited Γ] (L R : ListBlank Γ) :
    (Tape.mk' L R).move Dir.left = Tape.mk' L.tail (R.cons L.head) := by
  simp only [Tape.move, Tape.mk', ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]

Похожие утверждения