RG ⊊ LR

This file proves that regular languages form a strict subclass of LR languages.

The witness is the language {aⁿbⁿ}, which is LR(0) (via cfg_anbn) but not regular (by the pumping lemma). Combined with the already-established inclusion RG ⊆ LR, this gives strict containment.

Main results

• RG_strict_subclass_LR — RG ⊊ LR over any nontrivial finite alphabet.

theorem RG_strict_subclass_LR {T : Type} [Fintype T] [Nontrivial T] : RG ⊂ LR

Regular languages are a strict subclass of LR languages over any nontrivial finite alphabet.