Finite-support witnesses for indexed languages

Every indexed language has an indexed-grammar witness whose nonterminal and flag types are finite. This packages the grammar-level finite-support restriction for class-level use.

theorem is_Indexed_exists_finiteSupport_grammar {T : Type} {L : Language T} (hL : is_Indexed L) : ∃ (g : IndexedGrammar T) (x : Fintype g.nt) (x : Fintype g.flag), g.Language = L

Every indexed language has a grammar witness with finite nonterminal and flag types.

theorem is_Indexed_iff_exists_finiteSupport_grammar {T : Type} {L : Language T} : is_Indexed L ↔ ∃ (g : IndexedGrammar T) (x : Fintype g.nt) (x : Fintype g.flag), g.Language = L

Indexed languages are unchanged if their witnesses are required to use finite nonterminal and flag types.

theorem is_Indexed_noEpsilon_exists_finiteSupport_normalForm {T : Type} [Inhabited T] {L : Language T} (hL : is_Indexed_noEpsilon L) : ∃ (g : IndexedGrammar T) (x : Fintype g.nt) (x : Fintype g.flag) (x : DecidableEq g.nt), g.IsNormalForm ∧ g.Language = L

ε-free indexed languages have finite-support normal-form grammar witnesses.

theorem is_Indexed_noEpsilon_exists_fintype_normalForm_image {T : Type} [Inhabited T] {L : Language T} (hL : is_Indexed_noEpsilon L) : ∃ (A : Type) (x : Fintype A) (x : DecidableEq A) (x : Inhabited A) (f : A → T) (g : IndexedGrammar A) (x : Fintype g.nt) (x : Fintype g.flag) (x : DecidableEq g.nt), g.IsNormalForm ∧ (Language.map f) g.Language = L

Every ε-free indexed language is the image of a finite-alphabet, finite-support, normal-form indexed grammar.

This packages all reductions needed before the final indexed-to-CS simulation: the terminal alphabet, nonterminal type, and flag type are finite, the terminal alphabet is inhabited, and the grammar is in indexed normal form.

theorem is_Indexed_exists_fintype_normalForm_nonempty_image {T : Type} [Inhabited T] {L : Language T} (hL : is_Indexed L) : ∃ (A : Type) (x : Fintype A) (x : DecidableEq A) (x : Inhabited A) (f : A → T) (g : IndexedGrammar A) (x : Fintype g.nt) (x : Fintype g.flag) (x : DecidableEq g.nt), g.IsNormalForm ∧ (Language.map f) g.Language = L \ {[]}

Every indexed language has a finite-alphabet, finite-support, normal-form indexed grammar for its nonempty part. This is the class-level arbitrary-ε normal-form theorem: normal-form grammars are ε-free, so the empty word is handled separately by downstream context-sensitive closure lemmas.