English
If a mapping ss supports all statements of M on S and some q is in stmts M S, then q is supported.
Русский
Если отображение ss поддерживает все утверждения M на S, и q ∈ stmts M S, то q поддерживается.
LaTeX
$$stmts_supportsStmt (M,S) q ss : SupportsStmt S q$$
Lean4
/-- Translate a normal instruction. For the `write` command, we use a `goto` indirection so that
we can access the current value of the tape. -/
def trNormal : Stmt Γ Λ σ → Stmt Bool (Λ' Γ Λ σ) σ
| Stmt.move d q => move n d <| trNormal q
| Stmt.write f q => read dec fun a ↦ Stmt.goto fun _ s ↦ Λ'.write (f a s) q
| Stmt.load f q => read dec fun a ↦ (Stmt.load fun _ s ↦ f a s) <| trNormal q
| Stmt.branch p q₁ q₂ => read dec fun a ↦ Stmt.branch (fun _ s ↦ p a s) (trNormal q₁) (trNormal q₂)
| Stmt.goto l => read dec fun a ↦ Stmt.goto fun _ s ↦ Λ'.normal (l a s)
| Stmt.halt => Stmt.halt
