English
The set of translated statements is built from the TM1 stmts extended by all possibilities in Finite universe.
Русский
Переведённое множество утверждений строится из TM1 stmts и всех возможностей во множестве Finite.
LaTeX
$$trStmts (S) = TM1.stmts M S ×ˢ Finset.univ$$
Lean4
/-- Given a finite set of accessible `Λ` machine states, there is a finite set of accessible
machine states in the target (even though the type `Λ'` is infinite). -/
noncomputable def trStmts (S : Finset Λ) : Finset (Λ' M) :=
(TM1.stmts M S) ×ˢ Finset.univ