Indexed Languages Are Closed Under Regular Right Quotient

The proof uses the standard full-AFL factorization already established in the context-free quotient development. First substitute either a left or a right tag for every input symbol. Intersect with the regular language consisting of a left-tagged prefix followed by a right-tagged word in the quotient denominator. Finally substitute the left tags back to their symbols and erase the right tags.

The set-theoretic identity is independent of the language class. Indexed closure under substitution and intersection with a regular language therefore supplies the result directly.

theorem is_Indexed_rightQuotient_regular {T : Type} [Fintype T] {L R : Language T} (hL : is_Indexed L) (hR : R.IsRegular) : is_Indexed (L / R)

An indexed language right-quotiented by a regular language is indexed.

theorem Indexed_closedUnderRightQuotientWithRegular {T : Type} [Fintype T] : ClosedUnderRightQuotientWithRegular is_Indexed

Indexed languages are closed under right quotient with regular languages, uniformly over every finite alphabet.