Context-Sensitive Non-Closure Under Substitution

Context-sensitive 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 CS_notClosedUnderHomomorphism.

theorem CS_notClosedUnderSubstitution : ¬ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_CS

Context-sensitive languages are not closed under substitution.