RG ⊊ Linear

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

Main results

• exists_Linear_not_regular — There exists a linear language over Bool that is not regular.
• exists_Linear_not_regular_of_nontrivial — There exists a linear nonregular language over any nontrivial alphabet.
• RG_strict_subclass_Linear — Right-regular languages form a strict subclass of linear languages.

theorem exists_Linear_not_regular : ∃ (L : Language Bool), is_Linear L ∧ ¬L.IsRegular

There exists a linear language that is not regular.

theorem map_anbn_is_Linear {T : Type} (f : Bool → T) (_hf : Function.Injective f) : is_Linear ((Language.map f) anbn)

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

There exists a linear nonregular language over any nontrivial alphabet.

theorem RG_strict_subclass_Linear {T : Type} [Nontrivial T] : RG ⊂ Linear

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