Context-Sensitive Closure Under ε-Free Homomorphism

This file proves that context-sensitive languages are closed under string homomorphisms that do not erase symbols.

theorem is_CS_homomorphicImage_epsfree {α β : Type} (L : Language α) (h : α → List β) (heps : IsEpsFreeHomomorphism h) (hL : is_CS L) : is_CS (L.homomorphicImage h)

Context-sensitive languages are closed under ε-free string homomorphism, without requiring the ambient terminal types themselves to be finite.

theorem CS_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_CS

Context-sensitive languages are closed under ε-free string homomorphism.