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

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

theorem DCFA2nBnPosStar.DCF_quotientNumerator : is_DCF quotientNumerator

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