Indexed Languages Are Closed Under Inverse Homomorphism

The proof factors inverse homomorphism through a block coding. Its only substantial auxiliary ingredient is the standard indexed-grammar product with a DFA, used to intersect an indexed language with the regular block-code language.

theorem Indexed_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_Indexed

Indexed languages are closed under inverse string homomorphism.