Context-Sensitive Closure Under Union

We prove closure under union by first normalizing each context-sensitive grammar to an equivalent noncontracting grammar away from ε. Noncontracting grammars are closed under union by adding a fresh start symbol that jumps to either summand. If the original union contains ε, we add it back using the existing addEmpty construction.

theorem CS_closedUnderUnion {T : Type} : ClosedUnderUnion is_CS

Context-sensitive languages are closed under union.