Indexed Language Inclusions

This file proves that every context-free language is an indexed language.

The key idea: a context-free grammar can be viewed as an indexed grammar with an empty flag type (Empty). Since there are no flags, no rule consumes or pushes flags, and every nonterminal carries the trivial empty stack throughout derivations.

Main declarations

• indexed_of_cfg — convert a CF grammar to an equivalent indexed grammar
• CF_subclass_Indexed — CF ⊆ Indexed

def indexed_of_cfg {T : Type} (g : CF_grammar T) : IndexedGrammar T

Convert a context-free grammar to an indexed grammar (with no flags).

Equations

• One or more equations did not get rendered due to their size.

theorem indexed_of_cfg_language {T : Type} (g : CF_grammar T) : (indexed_of_cfg g).Language = CF_language g

The language of indexed_of_cfg g equals CF_language g.

theorem is_Indexed_of_is_CF {T : Type} {L : Language T} : is_CF L → is_Indexed L

Every context-free language is an indexed language.

theorem CF_subclass_Indexed {T : Type} : CF ⊆ Indexed

Every context-free language is an indexed language.