English
The function stmts(M,S) collects all statements reachable from the initial set S of labels, by taking the union of the immediate stmts from each label and inserting a bottom element.
Русский
Функция stmts(M,S) собирает все доступные инструкции из начального множества меток S, объединяя ближайшие stmts и добавляя нижний элемент.
LaTeX
$$$ stmts(M,S) = \operatorname{insertNone}\left( S \ biUnion_{q \in S} stmts_1(M(q)) \right) $$$
Lean4
/-- The set of statements accessible from initial set `S` of labels. -/
noncomputable def stmts (M : Λ → Stmt Γ Λ σ) (S : Finset Λ) : Finset (Option (Stmt Γ Λ σ)) :=
Finset.insertNone (S.biUnion fun q ↦ stmts₁ (M q))
