Idea: Construct a Grammar fragment for
$a^nb^(2n)$. Complement it with rules that break the symmetry.
1: L -> aaaX
2: X -> aXbb // So far, the subsequence of terminals does not belong to L.
// The next two rules break the symmetry.
3: X -> aP
4: X -> Qbb
5: P -> aP | epsilon
6: Q -> Qbb | epsilon
The grammar is clearly context-free.
The correctness can be proven eg. by induction over possible derivations. The intuition is simple:
Each derivation starts with applying rule 1 followed by an arbitrary number of. applications of rule 2. At each step of this derivation, the current item matches
a^3a^nXb^(2n); n >= 0. In particular,
n=min the nomenclature of the problem statement.
After application of any one of the rules 3 and 4, non-terminals will only ever expand into sequences of either
At least on application of rule 3 or 4 is necessary to complete a derivation.
The very first application of 3/4 introduces the imbalance between
bb in the terminal string. After passing that 'trapdoor', this imbalance will never be offset, since only the 'right' terminals will be produced henceforth.