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.