Context-Sensitive Languages Are Not Closed Under Right Quotient

The failure already occurs when the denominator is regular, so arbitrary right-quotient closure is impossible as well.

theorem CS_notClosedUnderRightQuotient : ¬ClosedUnderRightQuotient is_CS

Context-sensitive languages are not closed under arbitrary right quotient.

theorem CS_notClosedUnderRightQuotient_of_embedding {α : Type} [Fintype α] (e : Option Unit ↪ α) : ¬ClosedUnderRightQuotient is_CS

Context-sensitive languages are not closed under arbitrary right quotient over any finite alphabet into which the binary witness alphabet embeds.

theorem CS_notClosedUnderRightQuotient_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderRightQuotient is_CS

Context-sensitive languages are not closed under arbitrary right quotient over any finite alphabet with at least two symbols.