English
For any Tape T and integer i, after moving left, the nth element becomes the previous index: (T.move Dir.left).nth i = T.nth(i − 1).
Русский
Для любой ленты T и целого числа i, после перемещения влево, элемент на позиции i совпадает с элементом на позиции i−1: (T.move Dir.left).nth i = T.nth(i − 1).
LaTeX
$$$\forall {\Gamma} [Inhabited(\Gamma)] (T : Tape(\Gamma)) (i : \mathbb{Z}), (T.move Dir.left).nth i = T.nth (i - 1)$$$
Lean4
@[simp]
theorem move_left_nth {Γ} [Inhabited Γ] : ∀ (T : Tape Γ) (i : ℤ), (T.move Dir.left).nth i = T.nth (i - 1)
| ⟨_, _, _⟩, -(_ + 1 : ℕ) => (ListBlank.nth_succ _ _).symm
| ⟨_, _, _⟩, 0 => (ListBlank.nth_zero _).symm
| ⟨_, _, _⟩, 1 => (ListBlank.nth_zero _).trans (ListBlank.head_cons _ _)
| ⟨a, L, R⟩, (n + 1 : ℕ) + 1 => by
rw [add_sub_cancel_right]
change (R.cons a).nth (n + 1) = R.nth n
rw [ListBlank.nth_succ, ListBlank.tail_cons]
