Recursive Non-Closure Under Right Quotient By A Regular Language

Recursive languages are not closed under right quotient by a regular language.

The counterexample encodes the unary halting problem. Over Bool, let the regular suffix language be false*. The recursive numerator consists of words false^n ++ [true] ++ false^k such that the program encoded by n halts within bounded time k. Quotienting by false* removes the bounded-time certificate and leaves exactly the unbounded unary halting language on prefixes false^n ++ [true].

theorem Recursive_notClosedUnderRightQuotientWithRegular : ¬ClosedUnderRightQuotientWithRegular is_Recursive

Recursive languages are not closed under right quotient by regular languages.