Context-Free Closure Under Kleene Star

This file derives closure under Kleene star from closure under substitution.

Proof idea: use mathlib's context-free closure theorem for Kleene star and translate between mathlib's IsContextFree predicate and this repository's is_CF predicate.

Main declarations

• CF_of_star_CF

theorem CF_of_star_CF {T : Type} (L : Language T) : is_CF L → is_CF (KStar.kstar L)

The class of context-free languages is closed under Kleene star.

theorem CF_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar is_CF

The class of context-free languages is closed under Kleene star.