English
Let Γ be a type with an element and T a Tape Γ. Then for every integer i, the symbol at position i on the tape obtained by moving the head one position to the right equals the symbol at position i+1 on the original tape: (move_right T).nth i = T.nth (i+1).
Русский
Пусть Γ — тип с элементом, и T — лента над Γ. Тогда для каждого целого числа i символ в позиции i на ленте, полученной смещением головы вправо, равен символу в позиции i+1 исходной ленты: (move_right T).nth i = T.nth (i+1).
LaTeX
$$$ \forall \Gamma [\text{Inhabited } \Gamma]\ (T: \text{Tape } \Gamma)\ (i: \mathbb{Z}),\ (\text{move\_right}(T)).nth\ i = T.nth\ (i+1). $$$
Lean4
@[simp]
theorem move_right_nth {Γ} [Inhabited Γ] (T : Tape Γ) (i : ℤ) : (T.move Dir.right).nth i = T.nth (i + 1) :=
by
conv => rhs; rw [← T.move_right_left]
rw [Tape.move_left_nth, add_sub_cancel_right]
