Linear Language Inclusions

This file proves that every linear language is context-free.

Main results

• Linear_subclass_CF — Linear ⊆ CF

theorem grammar_context_free_of_linear {T : Type} {g : grammar T} (hg : grammar_linear g) : grammar_context_free g

A linear output is trivially a valid context-free output (no additional restriction).

theorem is_CF_of_is_Linear {T : Type} {L : Language T} (h : is_Linear L) : is_CF L

Every linear language is context-free.

theorem Linear_subclass_CF {T : Type} : Linear ⊆ CF

The class of linear languages is a subclass of the context-free languages.