Context-Free Union Bonus Construction

This file records a direct grammar construction for context-free closure under union.

Main declarations

• bonus_CF_of_CF_u_CF

def tacticGood_singleton : Lean.ParserDescr

Equations

• tacticGood_singleton = Lean.ParserDescr.node `tacticGood_singleton 1024 (Lean.ParserDescr.nonReservedSymbol "good_singleton" false)

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

An explicit grammar construction witnessing closure of context-free languages under union.