Finiteness of multi-tape Turing machine actions

With finitely many symbols and control states, there are finitely many one-step multi-tape Turing machine actions (Turing.Action.instFinite).

Main results

• Turing.Action.instFinite: Finite (Turing.Action k Symbol State) when Symbol and State are finite.

instance Turing.Action.instFinite {k : ℕ} {Symbol : Type u_1} {State : Type u_2} [Finite Symbol] [Finite State] : Finite (Action k Symbol State)

With finitely many states and symbols, there are finitely many actions.