English
For any finite case, the stmts₁ of halt is the singleton containing halt, i.e., stmts₁(halt) = {halt}.
Русский
Для конечного случая: stmts₁(halt) = {halt}.
LaTeX
$$$ \text{stmts}_1(\text{Stmt.halt}) = \mathcal{F}inset\,\{\text{Stmt.halt}\} $$$
Lean4
/-- The set of subtree statements in a statement. -/
noncomputable def stmts₁ : Stmt Γ Λ σ → Finset (Stmt Γ Λ σ)
| Q@(push _ _ q) => insert Q (stmts₁ q)
| Q@(peek _ _ q) => insert Q (stmts₁ q)
| Q@(pop _ _ q) => insert Q (stmts₁ q)
| Q@(load _ q) => insert Q (stmts₁ q)
| Q@(branch _ q₁ q₂) => insert Q (stmts₁ q₁ ∪ stmts₁ q₂)
| Q@(goto _) => { Q }
| Q@halt => { Q }