Context-Free Closure Under Concatenation

This file derives closure under concatenation from closure under substitution.

Proof idea: view L₁ * L₂ as a substitution instance of the singleton Boolean word language {[false, true]}. The substitution sends false to L₁ and true to L₂, so the substituted language is exactly all concatenations u ++ v with u ∈ L₁ and v ∈ L₂.

Main declarations

• CF_of_CF_c_CF

theorem CF_of_CF_c_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 concatenation.

theorem CF_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation is_CF

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