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.

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.