English
There is a confirmed one-step evolution from a configuration with a head at main to one with head at q, under the same structural conditions as before.
Русский
Существует проверяемый одноступенчатый переход из конфигурации с головой на main к конфигурации с головой на q, в тех же условиях.
LaTeX
$$$\\forall {q} {s} {L} {c} {d},\\;\\mathrm{Reaches}_1(\\mathrm{TM2.step}\\; tr)\\langle \\text{some}(\\mathrm{head\\ main}\\; q), s, K'.elim(\\mathrm{trList} L) [] c d\\rangle\n\\to\n \\langle \\text{some } q, \\text{none}, K'.elim(\\mathrm{trList} [L.headI]) [] c d\\rangle$$
Lean4
/-- The set of machine states reachable via downward label jumps, discounting jumps via `ret`. -/
def trStmts₁ : Λ' → Finset Λ'
| Q@(Λ'.move _ _ _ q) => insert Q <| trStmts₁ q
| Q@(Λ'.push _ _ q) => insert Q <| trStmts₁ q
| Q@(Λ'.read q) => insert Q <| Finset.univ.biUnion fun s => trStmts₁ (q s)
| Q@(Λ'.clear _ _ q) => insert Q <| trStmts₁ q
| Q@(Λ'.copy q) => insert Q <| trStmts₁ q
| Q@(Λ'.succ q) => insert Q <| insert (unrev q) <| trStmts₁ q
| Q@(Λ'.pred q₁ q₂) => insert Q <| trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)
| Q@(Λ'.ret _) => { Q }
