Context-Sensitive Closure Under Concatenation

Context-sensitive grammars in this library may have the distinguished start rule S -> epsilon. As in the union proof, we first replace each input language by a noncontracting grammar for its nonempty part. The unrestricted concatenation grammar from the RE development preserves noncontracting rules, so it gives a noncontracting grammar for the product of the nonempty parts. The nullable cases are then added back using context-sensitive union.

theorem CS_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation is_CS

Context-sensitive languages are closed under concatenation.