English
Let Γ be an inhabited type, T a Tape Γ, and i a natural number. Then the head after i successive moves to the right on T equals the i-th symbol of T.
Русский
Пусть Γ — тип с элементом и T — лента Γ. Тогда для каждого натурального i голова ленты после применения i правых сдвигов равна i-й позиции исходной ленты.
LaTeX
$$$ \forall \Gamma [\text{Inhabited } \Gamma] \ (T: \text{Tape } \Gamma)\ (i: \mathbb{N}),\ (\mathrm{move\_right})^{i}(T).head = T.nth\ i. $$$
Lean4
@[simp]
theorem move_right_n_head {Γ} [Inhabited Γ] (T : Tape Γ) (i : ℕ) : ((Tape.move Dir.right)^[i] T).head = T.nth i :=
by
induction i generalizing T
· rfl
· simp only [*, Tape.move_right_nth, Int.natCast_succ, iterate_succ, Function.comp_apply]
