The unary {a^(2^(k+1))} language

This file defines the unary language {a^(2^(k+1)) | k in N} over Bool, with false = a, and proves it is not context-free.

theorem notCF_unaryPow2 : ¬is_CF unaryPow2

The unary powers-of-two language is not context-free.

After pumping a word of length 2^(p+2), the new length is strictly between consecutive powers of two.