Deterministic Context-Free Non-Closure Under Intersection

This file transfers the existing CFL intersection counterexample to DCFLs by giving deterministic presentations of the two witness languages.

theorem DCF_notClosedUnderIntersection_of_lang_eq_any_witnesses (hEqAny : is_DCF lang_eq_any) (hAnyEq : is_DCF lang_any_eq) : ¬ClosedUnderIntersection is_DCF

The existing CFL intersection witnesses also disprove DCFL intersection closure once they are shown deterministic context-free.

theorem DCF_notClosedUnderIntersection : ¬ClosedUnderIntersection is_DCF

Deterministic context-free languages over Fin 3 are not closed under intersection.

theorem DCF_notClosedUnderIntersection_of_three {α : Type} [Fintype α] (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : ¬ClosedUnderIntersection is_DCF

Deterministic context-free languages are not closed under intersection for any finite alphabet containing three distinct symbols.

theorem DCF_notClosedUnderIntersection_of_card {α : Type} [Fintype α] (hα : 3 ≤ Fintype.card α) : ¬ClosedUnderIntersection is_DCF

Deterministic context-free languages are not closed under intersection for any finite alphabet with at least three symbols.