stmts₁ — Mathlib

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 }

Похожие утверждения