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

• is_Indexed_lang_eq_eq — {aⁿbⁿcⁿ} is an indexed language
• CF_strict_subclass_Indexed — CF ⊊ Indexed

inductive ANBNCN_NT : Type

Nonterminals for the aⁿbⁿcⁿ indexed grammar.

• S : ANBNCN_NT
• T : ANBNCN_NT
• A : ANBNCN_NT
• B : ANBNCN_NT
• C : ANBNCN_NT

instance instDecidableEqANBNCN_NT : DecidableEq ANBNCN_NT

Equations

• instDecidableEqANBNCN_NT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ANBNCN_Flag : Type

Flags for the aⁿbⁿcⁿ indexed grammar.

• count : ANBNCN_Flag
• bottom : ANBNCN_Flag

instance instDecidableEqANBNCN_Flag : DecidableEq ANBNCN_Flag

Equations

• instDecidableEqANBNCN_Flag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def grammar_anbncn_indexed : IndexedGrammar (Fin 3)

Equations

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

theorem is_Indexed_lang_eq_eq : is_Indexed lang_eq_eq