Regular Languages Included in Linear Languages

This file proves that every regular language is linear by showing that right-regular productions are linear productions.

Main results

• is_Linear_of_is_RG — every regular language is linear
• RG_subclass_Linear — RG ⊆ Linear

theorem linear_output_of_right_regular {T N : Type} {s : List (symbol T N)} (h : right_regular_output s) : linear_output s

A right-regular output has linear form.

theorem grammar_linear_of_right_regular {T : Type} {g : grammar T} (hg : grammar_right_regular g) : grammar_linear g

A right-regular grammar is linear.

theorem is_Linear_of_is_RG {T : Type} {L : Language T} (h : is_RG L) : is_Linear L

Every regular language is linear.

theorem RG_subclass_Linear {T : Type} : RG ⊆ Linear

The class of regular languages is a subclass of the linear languages.