Elementary Recursive Languages

This file records the immediate recursive languages, witnessed by TM0 machines that halt without taking a step.

theorem is_Recursive_univ {T : Type} : is_Recursive Set.univ

The universal language is recursive.

theorem is_Recursive_empty {T : Type} : is_Recursive ∅

The empty language is recursive.