Regular Languages Included in Deterministic Context-Free Languages

This file proves that every regular language over a finite alphabet is deterministic context-free.

Main results

• is_DCF_of_is_RG — every regular language is deterministic context-free
• RG_subclass_DCF — RG ⊆ DCF

theorem is_DCF_of_is_RG {T : Type} [Fintype T] {L : Language T} (h : is_RG L) : is_DCF L

Every right-regular language over a finite alphabet is a DCF.

theorem RG_subclass_DCF {T : Type} [Fintype T] : RG ⊆ DCF