English
Starting from a configuration with the head on the stack, the machine reaches a configuration with updated head and a transformed stack reflecting L₂ and L₃.
Русский
Из конфигурации с головой на стеке машина достигает конфигурации с обновленной головой и переработанным стеком, отражающим L₂ и L₃.
LaTeX
$$$\\forall q,s,L_1,L_2,L_3:\\quad\n \\mathrm{Reaches}_1(\\mathrm{TM2.step}\\; tr)\n\\langle \\mathrm{some}(\\mathrm{head\\ stack}\\; q), s, K'.elim (\\mathrm{trList }L_1) \\;[] \\; [] (\\mathrm{trList }L_2 \\;++\\; \\Gamma'.cons_{\\ell} :: L_3)\\rangle\n\\to\n \\langle \\mathrm{some}~q, \\mathrm{none}, K'.elim (\\mathrm{trList}(L_2.headI :: L_1)) \\;[] \\; [] L_3 \\rangle$$
Lean4
theorem head_stack_ok {q s L₁ L₂ L₃} :
Reaches₁ (TM2.step tr) ⟨some (head stack q), s, K'.elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)⟩
⟨some q, none, K'.elim (trList (L₂.headI :: L₁)) [] [] L₃⟩ :=
by
rcases L₂ with - | ⟨a, L₂⟩
· refine
TransGen.trans (move_ok (by decide) (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
(TransGen.head rfl (TransGen.head rfl ?_))
rw [tr]
simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append, elim_update_stack,
elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self, List.headI_nil, trNat_default]
convert unrev_ok using 2
simp
· refine
TransGen.trans
(move_ok (by decide)
(splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃) (trNat_natEnd _) ⟨rfl, by simp⟩))
(TransGen.head rfl (TransGen.head rfl ?_))
simp only [TM2.step, Option.mem_def, trList, List.append_assoc, List.cons_append, elim_update_stack, elim_rev,
elim_update_rev, Function.update_self, List.headI_cons]
refine
TransGen.trans
(clear_ok
(splitAtPred_eq _ _ (trList L₂) (some Γ'.consₗ) L₃ (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h))
⟨rfl, by simp⟩))
?_
convert unrev_ok using 2
simp [List.reverseAux_eq]
