English
Moving the TM1 head before a step corresponds to applying stepAux after performing the move n times on the tape.
Русский
Перед шагом Тьюринга головка tm1 смещается на n позиций, а затем выполняется шаг; это эквивалентно применению stepAux после n повторений перемещения ленты.
LaTeX
$$$\text{stepAux}(\text{move } n\, d\, q)\; v\; T = \text{stepAux}(q)\; v\; ((\text{Tape.move } d)^{[n]}\, T).$$$
Lean4
theorem stepAux_move (d : Dir) (q : Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (T : Tape Bool) :
stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T) :=
by
suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n
intro i
induction i generalizing T with
| zero => rfl
| succ i IH =>
rw [iterate_succ', iterate_succ]
simp only [stepAux, Function.comp_apply]
rw [IH]
