Indexed Languages Are Closed Under Substitution

The construction combines an outer indexed grammar with one tagged inner grammar for every source letter. An outer terminal production launches the initial nonterminal of the corresponding inner grammar. Outer and inner flags use disjoint tags, so the independent derivations can be separated again.

theorem Indexed_closedUnderSubstitution : ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_Indexed

Indexed languages are closed under substitution.