The {b^n a^n | n >= 1}* {b} Language as a DCF

This file builds the deterministic pushdown automaton for the denominator witness used in the right-quotient counterexample, with false = a and true = b.

theorem DCFBnAnPosStarB.DCF_quotientDenominator : is_DCF quotientDenominator

The language {b^n a^n | n >= 1}* {b} is deterministic context-free.