English
Equality of top-level tape translation under enc/dec choices.
Русский
Равенство перевода ленты в верхнем уровне при выборе enc/dec.
LaTeX
$$trTape_eq_1 (enc) (dec) (M) (L) (R) : trTape enc0 (Tape.mk' L R) = trTape' enc0 L R$$
Lean4
theorem trTape'_move_left (L R : ListBlank Γ) :
(Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (R.cons L.head) :=
by
obtain ⟨a, L, rfl⟩ := L.exists_cons
simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]
suffices
∀ {L' R' l₁ l₂} (_ : List.Vector.toList (enc a) = List.reverseAux l₁ l₂),
(Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
Tape.mk' L' (ListBlank.append (List.Vector.toList (enc a)) R')
by simpa only [List.length_reverse, Vector.toList_length] using this (List.reverse_reverse _).symm
intro _ _ l₁ l₂ e
induction l₁ generalizing l₂ with
| nil => cases e; rfl
| cons b l₁ IH =>
simp only [List.length, iterate_succ_apply]
convert IH e
simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]
