Strict Inclusion: CF ⊊ Indexed

This file proves that the class of indexed languages strictly contains the class of context-free languages, by exhibiting a witness: the language {aⁿbⁿcⁿ | n ∈ ℕ} is indexed but not context-free.

The indexed grammar uses a stack-bottom marker to ensure that each nonterminal consumes exactly as many flags as were pushed.

Main declarations

• CF_strict_subclass_Indexed — CF ⊂ Indexed

theorem CF_subclass_Indexed_and_exists_strict : (∀ (T : Type) (L : Language T), is_CF L → is_Indexed L) ∧ ∃ (T : Type) (L : Language T), is_Indexed L ∧ ¬is_CF L

CF ⊊ Indexed: context-free languages form a strict subclass of indexed languages.

theorem CF_strict_subclass_Indexed {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) : CF ⊂ Indexed

For any finite alphabet with at least 3 symbols, context-free languages form a strict subclass of indexed languages.