stmts₁ — Mathlib

English

The subterm closure of a statement is the finite set of all substatements reachable via structural recursion.

Русский

Поддерево подвыражений — конечное множество всех подпредикатов, достижимых через структурное рекурсирование.

LaTeX

$$$\\mathrm{stmts}_1 : \\mathrm{Stmt}\\ \\Gamma\\ \\Lambda\\ \\sigma \\to \\mathrm{Finset}\\ (\\mathrm{Stmt}\\ \\Gamma\\ \\Lambda\\ \\sigma)$$$

Lean4

/-- The subterm closure of a statement. -/
noncomputable def stmts₁ : Stmt Γ Λ σ → Finset (Stmt Γ Λ σ)
  | Q@(move _ q) => insert Q (stmts₁ q)
  | Q@(write _ q) => insert Q (stmts₁ q)
  | Q@(load _ q) => insert Q (stmts₁ q)
  | Q@(branch _ q₁ q₂) => insert Q (stmts₁ q₁ ∪ stmts₁ q₂)
  | Q => { Q }

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