stmts — Mathlib

English

Equality between the STM1 statement set and a constructed embedding of stmts₁ over M q.

Русский

Равенство множества утверждений STM1 и сконструированного вложения stmts₁ по M q.

LaTeX

$$Eq (Turing.TM1.stmts M S) (RelEmbedding.instFunLike.coe Finset.insertNone (S.biUnion fun q => Turing.TM1.stmts₁ (M q)))$$

Lean4

/-- The set of all statements in a Turing machine, plus one extra value `none` representing the
halt state. This is used in the TM1 to TM0 reduction. -/
noncomputable def stmts (M : Λ → Stmt Γ Λ σ) (S : Finset Λ) : Finset (Option (Stmt Γ Λ σ)) :=
  Finset.insertNone (S.biUnion fun q ↦ stmts₁ (M q))

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