trSupp — Mathlib

English

From a program, collect all write-accessible machine states into a finite set.

Русский

Из программы собрать множество состояний машины, достижимых записью, в конечное множество.

LaTeX

$$$$\\text{writes}:\\; \\text{Stmt } \\Gamma \\Lambda \\sigma \\to \\mathcal{F}inset(\\Lambda'\\Gamma\\Lambda\\sigma). $$$$

Lean4

/-- The set of accessible machine states, assuming that the input machine is supported on `S`,
are the normal states embedded from `S`, plus all write states accessible from these states. -/
noncomputable def trSupp (S : Finset Λ) : Finset (Λ' Γ Λ σ) :=
  S.biUnion fun l ↦ insert (Λ'.normal l) (writes (M l))

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