Indexed languages are not closed under arbitrary right quotient #

For the binary intersection witnesses A and B, the balanced-copy numerator and denominator from Langlib.Examples.AbnPowMCopy have right quotient equal to the injective image of A ∩ B = {(a b^n)^n | n > 0}. Both operands are indexed, while the shrinking theorem shows that this diagonal quotient is not indexed.

source

theorem abnPowMCopy_quotient_not_is_Indexed :

¬is_Indexed (abnPowMCopy / abnPowMCopyDenominator)

The quotient result itself is not indexed.

source

theorem Indexed_notClosedUnderRightQuotient :

¬ClosedUnderRightQuotient is_Indexed

Indexed languages over the three-symbol copy alphabet are not closed under arbitrary right quotient.

source

theorem Indexed_notClosedUnderRightQuotient_of_embedding {alpha : Type} (e : CopyLetter ↪ alpha) :

¬ClosedUnderRightQuotient is_Indexed

Nonclosure transports to every alphabet containing the three-symbol witness alphabet.

source

theorem Indexed_notClosedUnderRightQuotient_of_card {alpha : Type} [Fintype alpha] (halpha : 3 ≤ Fintype.card alpha) :

¬ClosedUnderRightQuotient is_Indexed

Indexed languages are not closed under arbitrary right quotient over every finite alphabet with at least three symbols.