trTape'_move_right — Mathlib

English

Left-move iteration preserves structure of trTape' under nested moves.

Русский

Левый сдвиг сохраняет структуру trTape' при вложенных сдвигах.

LaTeX

$$trTape'_move_left (L R) : (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (R.cons L.head)$$

Lean4

theorem trTape'_move_right (L R : ListBlank Γ) :
    (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (L.cons R.head) R.tail :=
  by
  suffices ∀ i L, (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
    by
    refine (Eq.symm ?_).trans (this n _)
    simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons, ListBlank.tail_cons]
  intro i _
  induction i with
  | zero => rfl
  | succ i IH => rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]

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