English
From a configuration with the main-head at q, there is a one-step evolution to a configuration with the head at q and the stack prepared by the next instruction.
Русский
Из конфигурации с главным узлом на q существует одноступенчатое переходное состояние к конфигурации, где голова на q, а стек подготовлен следующей инструкцией.
LaTeX
$$$\\forall q,s,L,c,d,\\, \\mathrm{Reaches}_1(\\mathrm{TM2.step}\\; tr)\n\\Big(\\langle \\mathrm{some}(\\mathrm{head\\ main}\\; q), s, K'.elim(\\mathrm{trList }L)\\;[]\\; c\\; d\\rangle\\Big)\n=\\Big(\\langle \\mathrm{some}~q, \\mathrm{none}, K'.elim(\\mathrm{trList}[L.headI])\\;[]\\; c\\; d\\rangle\\Big)\$$
Lean4
theorem head_main_ok {q s L} {c d : List Γ'} :
Reaches₁ (TM2.step tr) ⟨some (head main q), s, K'.elim (trList L) [] c d⟩
⟨some q, none, K'.elim (trList [L.headI]) [] c d⟩ :=
by
let o : Option Γ' := List.casesOn L none fun _ _ => some Γ'.cons
refine
(move_ok (by decide) (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
(TransGen.head rfl (TransGen.head rfl ?_))
· cases L <;> simp [o]
rw [tr]
simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev, Function.update_self,
trList]
rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])]
refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_
· exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)
convert unrev_ok using 2; simp [List.reverseAux_eq]
