Deterministic Context-Free Languages Are Not Closed Under Kleene Star

The proof uses the standard DCFL union witnesses, restricted to strictly positive a, b, and c blocks. The positive restriction prevents a later Kleene-star slice from decomposing one a+ b+ c+ payload into several witness blocks.

theorem DCFStar.DCF_notClosedUnderUnion_pos : ¬ClosedUnderUnion is_DCF

theorem DCFStar.DCF_notClosedUnderKleeneStar : ¬ClosedUnderKleeneStar is_DCF

Deterministic context-free languages over Bool ⊕ Fin 3 are not closed under Kleene star.

theorem DCFStar.DCF_notClosedUnderKleeneStar_of_embedding {α : Type} [Fintype α] (e : Bool ⊕ Fin 3 ↪ α) : ¬ClosedUnderKleeneStar is_DCF

DCFLs are not closed under Kleene star over any finite alphabet into which the five-symbol witness alphabet embeds.

theorem DCFStar.DCF_notClosedUnderKleeneStar_of_card {α : Type} [Fintype α] (hα : 5 ≤ Fintype.card α) : ¬ClosedUnderKleeneStar is_DCF

DCFLs are not closed under Kleene star over any finite alphabet with at least five symbols.