Deterministic Context-Free Right Quotients

This file proves that deterministic context-free languages are not closed under right quotient. The witness is the same quotient used for CFL non-closure:

• quotientNumerator = {a^(2n)b^n | n >= 1}*
• quotientDenominator = {b^n a^n | n >= 1}* {b}

Both witness languages are deterministic context-free, by the DPDAs in DeterministicContextFree/Examples. If DCFLs were closed under right quotient, their quotient would be a DCFL and therefore context-free, contradicting the CFL pumping argument already proved in ContextFree/Closure/Quotient.

theorem DCF_notClosedUnderRightQuotient : ¬ClosedUnderRightQuotient is_DCF

Deterministic context-free languages are not closed under right quotient.