Indexed Languages Are Closed Under String Homomorphism

This file maps terminal symbols in indexed grammar right-hand sides to strings of terminals while preserving nonterminals and their stacks.

Proof idea: replace each terminal occurrence in every rule by the corresponding output string and leave indexed nonterminals unchanged. The derivation translation maps each sentential form by the same terminal expansion, giving exactly the homomorphic image of the generated language.

theorem Indexed_closedUnderHomomorphism : ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_Indexed

Indexed languages are closed under string homomorphism.

theorem Indexed_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_Indexed

Indexed languages are closed under ε-free string homomorphism.