Deterministic Context-Free Closure Under Union With Regular Languages

This is a derived closure fact, not full union closure for deterministic context-free languages. The proof uses De Morgan together with complement closure and closure under intersection with regular languages.

theorem DCF_union_regular {T : Type} [Fintype T] (L R : Language T) (hL : is_DCF L) (hR : R.IsRegular) : is_DCF (L + R)

Union of a DCF language with a regular language is DCF.

theorem DCF_regular_union {T : Type} [Fintype T] (R L : Language T) (hR : R.IsRegular) (hL : is_DCF L) : is_DCF (R + L)

Union of a regular language with a DCF language is DCF.