RG ⊊ CF

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

Main results

• exists_CF_not_regular — There exists a CF language over Bool that is not regular.
• exists_CF_not_regular_of_nontrivial — There exists a CF nonregular language over any nontrivial alphabet.
• RG_strict_subclass_CF — Right-regular languages form a strict subclass of CF languages.

theorem exists_CF_not_regular : ∃ (L : Language Bool), is_CF L ∧ ¬L.IsRegular

There exists a context-free language that is not regular.

theorem exists_CF_not_regular_of_nontrivial {T : Type} [Nontrivial T] : ∃ (L : Language T), is_CF L ∧ ¬L.IsRegular

There exists a context-free nonregular language over any nontrivial alphabet.

theorem RG_strict_subclass_CF {T : Type} [Nontrivial T] : RG ⊂ CF

Right-regular languages form a strict subclass of context-free languages over any nontrivial alphabet.