Lean4
/-- The raw definition of a Turing machine does not require that
`Γ` and `Λ` are finite, and in practice we will be interested
in the infinite `Λ` case. We recover instead a notion of
"effectively finite" Turing machines, which only make use of a
finite subset of their states. We say that a set `S ⊆ Λ`
supports a Turing machine `M` if `S` is closed under the
transition function and contains the initial state. -/
def Supports (M : Machine Γ Λ) (S : Set Λ) :=
default ∈ S ∧ ∀ {q a q' s}, (q', s) ∈ M q a → q ∈ S → q' ∈ S