The positive {a^(2n)b^n} language

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

theorem quotientLeftBlock_eq_singletons_core : quotientLeftBlock = {[false, false]} * quotientLeftBlockCore * {[true]}

theorem CF_quotientLeftBlock : is_CF quotientLeftBlock