English
A finite set S of labels supports a TM1 statement if all goto targets lie inside S and leaves halt as true.
Русский
Конечный набор меток S поддерживает оператор TM1, если все goto ссылаются внутрь S, а halt истинно.
LaTeX
$$$\\forall S,\\ \\mathrm{SupportsStmt}\\ S\\; (\\mathrm{Stmt})$ (определение) [подробности: move, write, load, branch, goto, halt]$$
Lean4
/-- A set `S` of labels supports the statement `q` if all the `goto`
statements in `q` refer only to other functions in `S`. -/
def SupportsStmt (S : Finset Λ) : Stmt Γ Λ σ → Prop
| move _ q => SupportsStmt S q
| write _ q => SupportsStmt S q
| load _ q => SupportsStmt S q
| branch _ q₁ q₂ => SupportsStmt S q₁ ∧ SupportsStmt S q₂
| goto l => ∀ a v, l a v ∈ S
| halt => True
