English
If a structure ss supports M on S, then the result of stepping preserves supports on S.
Русский
Если ss поддерживает M на S, то переход шага сохраняет поддержку на S.
LaTeX
$$step_supports (M) (ss) : Supports M S -> Supports (tr M) (trStmts M S)$$
Lean4
/-- The core TM1 → TM0 translation function. Here `s` is the current value on the tape, and the
`Stmt₁` is the TM1 statement to translate, with local state `v : σ`. We evaluate all regular
instructions recursively until we reach either a `move` or `write` command, or a `goto`; in the
latter case we emit a dummy `write s` step and transition to the new target location. -/
def trAux (s : Γ) : TM1.Stmt Γ Λ σ → σ → Λ' M × TM0.Stmt Γ
| TM1.Stmt.move d q, v => ((some q, v), move d)
| TM1.Stmt.write a q, v => ((some q, v), write (a s v))
| TM1.Stmt.load a q, v => trAux s q (a s v)
| TM1.Stmt.branch p q₁ q₂, v => cond (p s v) (trAux s q₁ v) (trAux s q₂ v)
| TM1.Stmt.goto l, v => ((some (M (l s v)), v), write s)
| TM1.Stmt.halt, v => ((none, v), write s)
