Recursive Closure Under Intersection With Regular Languages

This file proves that recursive languages are closed under intersection with a regular language.

The proof composes the computable membership predicate for the recursive language with the DFA-derived computable membership predicate for the regular language.

theorem is_Recursive_intersection_regular {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L R : Language T} (hL : is_Recursive L) (hR : R.IsRegular) : is_Recursive (L ⊓ R)

Recursive languages are closed under intersection with regular languages.

theorem Recursive_closedUnderIntersectionWithRegular {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderIntersectionWithRegular is_Recursive

The class of recursive languages is closed under intersection with regular languages.