DCFs are a strict subset of CFLs

This file records the closure-mismatch route to strictness for the inclusion DCF ⊆ CF.

theorem DCF_strict_subclass_CF_of_closedUnderComplement (hDCFcomp : ClosedUnderComplement is_DCF) : DCF ⊂ CF

If deterministic context-free languages are closed under complement over Fin 3, then they form a strict subclass of context-free languages over Fin 3.

This isolates the useful closure-property proof pattern behind the unconditional strictness theorem below.

theorem DCF_strict_subclass_CF_of_closedUnderComplement_of_three {T : Type} [Fintype T] (a b c : T) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hDCFcomp : ClosedUnderComplement is_DCF) : DCF ⊂ CF

If deterministic context-free languages are closed under complement over an alphabet with three distinguished symbols, then they form a strict subclass of context-free languages over that alphabet.

theorem DCF_strict_subclass_CF_of_closedUnderComplement_of_card {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) (hDCFcomp : ClosedUnderComplement is_DCF) : DCF ⊂ CF

If deterministic context-free languages are closed under complement over a finite alphabet with at least three symbols, then they form a strict subclass of context-free languages over that alphabet.

theorem DCF_strict_subclass_CF : DCF ⊂ CF

Deterministic context-free languages are a strict subclass of context-free languages over a three-symbol alphabet.

theorem DCF_strict_subclass_CF_of_card {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) : DCF ⊂ CF

Deterministic context-free languages are a strict subclass of context-free languages over any finite alphabet with at least three symbols.