RG ⊊ DCF

This file uses the example language {aⁿbⁿ} to show that regular languages form a strict subclass of deterministic context-free languages.

Main results

• RG_strict_subclass_DCF — Regular languages are a strict subclass of DCFs.
• RG_strict_subclass_DCF_of_card — The inclusion over every finite alphabet with at least 2 elements.

theorem RG_strict_subclass_DCF {T : Type} [Fintype T] [Nontrivial T] : RG ⊂ DCF

Regular languages are a strict subclass of deterministic context-free languages over any nontrivial alphabet.

theorem RG_strict_subclass_DCF_of_card {T : Type} [Fintype T] (hT : 2 ≤ Fintype.card T) : RG ⊂ DCF

Regular languages are a strict subclass of deterministic context-free languages over every finite alphabet with at least 2 elements.