The positive {b^n a^n} language

This file defines {b^n a^n | n >= 1} over Bool, with false = a and true = b, and proves it is context-free.

theorem quotientRightBlock_eq_singletons_core : quotientRightBlock = {[true]} * quotientRightBlockCore * {[false]}

theorem CF_quotientRightBlock : is_CF quotientRightBlock