RE Closure Under Union

This file constructs an unrestricted grammar for the union of two recursively enumerable languages.

Proof idea: build a grammar with a fresh start symbol that chooses either the left or right grammar, then run the chosen grammar with all its nonterminals tagged. The soundness and completeness lemmas project derivations through the tags, showing the combined grammar generates exactly L₁ + L₂.

Main declarations

• union_grammar
• in_L₁_or_L₂_of_in_union
• in_union_of_in_L₁
• in_union_of_in_L₂
• RE_of_RE_u_RE

def union_grammar {T : Type} (g₁ g₂ : grammar T) : grammar T

Equations

• One or more equations did not get rendered due to their size.

theorem in_L₁_or_L₂_of_in_union {T : Type} {g₁ g₂ : grammar T} {w : List T} (ass : w ∈ grammar_language (union_grammar g₁ g₂)) : w ∈ grammar_language g₁ ∨ w ∈ grammar_language g₂

theorem in_union_of_in_L₁ {T : Type} {g₁ g₂ : grammar T} {w : List T} (ass : w ∈ grammar_language g₁) : w ∈ grammar_language (union_grammar g₁ g₂)

theorem in_union_of_in_L₂ {T : Type} {g₁ g₂ : grammar T} {w : List T} (ass : w ∈ grammar_language g₂) : w ∈ grammar_language (union_grammar g₁ g₂)

theorem RE_of_RE_u_RE {T : Type} (L₁ L₂ : Language T) : is_RE L₁ ∧ is_RE L₂ → is_RE (L₁ + L₂)

The class of recursively-enumerable languages is closed under union.

theorem RE_closedUnderUnion {T : Type} : ClosedUnderUnion is_RE

The class of recursively enumerable languages is closed under union.