Regular Languages Are Recursive

This file converts a finite-state DFA into a TM0 decider by scanning right across the input while carrying the DFA state in the TM0 state.

theorem RecursiveRegular.is_Recursive_of_dfa {α σ : Type} [Fintype σ] (M : DFA α σ) : is_Recursive M.accepts

theorem is_Recursive_of_isRegular {α : Type} {L : Language α} (hL : L.IsRegular) : is_Recursive L

theorem is_Recursive_singleton_word {α : Type} (w : List α) : is_Recursive {w}

Every singleton word language is recursive.