Context-Free Closure Under Union

This file derives closure under union from closure under substitution.

Proof idea: view L₁ ∪ L₂ as a substitution instance of the two-word Boolean language {[false], [true]}. The substitution sends false to L₁ and true to L₂, so choosing one of the two singleton words chooses one of the two component languages.

Main declarations

• CF_of_CF_u_CF

theorem CF_of_CF_u_CF {T : Type} (L₁ L₂ : Language T) : is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ + L₂)

The class of context-free languages is closed under union.

theorem CF_closedUnderUnion {T : Type} : ClosedUnderUnion is_CF

The class of context-free languages is closed under union.