English
The auxiliary step after a read operation corresponds to applying the continuation function to the head of the right-hand tape and then continuing with the left tape unchanged.
Русский
После операции считывания вспомогательный шаг соответствует применению продолжения функции к голове правой части ленты, затем продолжение с левым куском ленты без изменений.
LaTeX
$$$$\\operatorname{stepAux}(\\operatorname{read} \\; dec\\; f)\\; v\\; \\operatorname{trTape}'(\\operatorname{enc0}, L, R) = \\operatorname{stepAux}(f\\; (R.head))\\; v\\; \\operatorname{trTape}'(\\operatorname{enc0}, L, R). $$$$
Lean4
theorem stepAux_read (f : Γ → Stmt Bool (Λ' Γ Λ σ) σ) (v : σ) (L R : ListBlank Γ) :
stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R) :=
by
suffices
∀ f, stepAux (readAux n f) v (trTape' enc0 L R) = stepAux (f (enc R.head)) v (trTape' enc0 (L.cons R.head) R.tail)
by
rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]
simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]
obtain ⟨a, R, rfl⟩ := R.exists_cons
simp only [ListBlank.head_cons, ListBlank.tail_cons, trTape', ListBlank.cons_flatMap]
suffices
∀ i f L' R' l₁ l₂ h,
stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
by
intro f
exact this n f (L.flatMap (fun x => (enc x).1.reverse) _) (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2
clear f L a R
intro i f L' R' l₁ l₂ _
subst i
induction l₂ generalizing l₁ with
| nil => rfl
| cons a l₂
IH =>
trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
· dsimp [readAux, stepAux]
simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
cases a <;> rfl
· rw [← ListBlank.append, IH]
rfl
