Recursive Non-Closure Under Substitution

Recursive languages are not closed under finite-alphabet substitution. If they were, then substituting each source symbol by the singleton language containing its homomorphic image would imply closure under arbitrary string homomorphism, contradicting Recursive_notClosedUnderHomomorphism.

theorem Recursive_notClosedUnderSubstitution : ¬ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_Recursive

Recursive languages are not closed under substitution.