RE Closure Under Kleene Star

This file proves that the class of recursively enumerable languages is closed under Kleene star. The proof constructs an unrestricted grammar for L* given an unrestricted grammar for L, following the construction from the Lean 3 proof RE_star.lean.

Grammar Construction

Given a grammar g for L with nonterminals N and start symbol S:

• New nonterminals: Z (start), H (separator), R (scanner), plus lifted originals
• Rules:
  1. Z → Z S H (generate another copy)
  2. Z → R H (start terminal scanning)
  3. R H → R (scanner jumps over separator)
  4. R H → ε (scanner+separator deleted at end)
  5. All original rules (with nonterminals lifted)
  6. R t → t R for each terminal t (scanner moves left past terminals)

Main declarations

• RE_of_star_RE — the main closure theorem

theorem RE_of_star_RE {T : Type} (L : Language T) : is_RE L → is_RE (KStar.kstar L)

The class of recursively enumerable languages is closed under the Kleene star.

theorem RE_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar is_RE

The class of recursively enumerable languages is closed under Kleene star.