English
There is a step from the successor of q to q itself in one move, aligning with the numerical increment n to n+1.
Русский
Существует переход от succ(q) к q за один шаг, соответствующий приращению n к n+1.
LaTeX
$$$\\forall q\\;\\text{for Nat } n:\\; \\mathrm{Reaches}_1(\\mathrm{TM2.step}\\; tr)\n\\langle \\mathrm{some}(\\Lambda'.succ q), s, K'.elim (\\mathrm{trList} [n]) \\;[] \\; c \\; d\\rangle\n\\to\n \\langle \\mathrm{some}~q, \\mathrm{none}, K'.elim (\\mathrm{trList} [n.succ]) \\;[] \\; c \\; d\\rangle$$
Lean4
theorem succ_ok {q s n} {c d : List Γ'} :
Reaches₁ (TM2.step tr) ⟨some (Λ'.succ q), s, K'.elim (trList [n]) [] c d⟩
⟨some q, none, K'.elim (trList [n.succ]) [] c d⟩ :=
by
simp only [trList, trNat.eq_1, Nat.cast_succ, Num.add_one]
rcases (n : Num) with - | a
· refine TransGen.head rfl ?_
simp only [Option.mem_def]
convert unrev_ok using 1
simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]
rfl
simp only [trNum, Num.succ, Num.succ']
suffices
∀ l₁,
∃ l₁' l₂' s',
List.reverseAux l₁ (trPosNum a.succ) = List.reverseAux l₁' l₂' ∧
Reaches₁ (TM2.step tr) ⟨some q.succ, s, K'.elim (trPosNum a ++ [Γ'.cons]) l₁ c d⟩
⟨some (unrev q), s', K'.elim (l₂' ++ [Γ'.cons]) l₁' c d⟩
by
obtain ⟨l₁', l₂', s', e, h⟩ := this []
simp only [List.reverseAux] at e
refine h.trans ?_
convert unrev_ok using 2
simp [e, List.reverseAux_eq]
induction a generalizing s with intro l₁
| one =>
refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
simp [trPosNum]
| bit1 m IH =>
obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
simp [trPosNum]
rfl
| bit0 m _ =>
refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
simp only [TM2.step]; rw [tr]
simp only [TM2.stepAux, pop', elim_main, elim_update_main, elim_rev, elim_update_rev, Function.update_self,
Option.mem_def, Option.some.injEq]
rfl
