Context free grammar for this language
Idea: Construct a Grammar fragment for $a^nb^(2n)$. Complement it with rules that break the symmetry.

1: L -&gt; aaaX

2: X -&gt; aXbb   // So far, the subsequence of terminals does not belong to L. 
               // The next two rules break the symmetry. 
3: X -&gt; aP
4: X -&gt; Qbb

5: P -&gt; aP  | epsilon
6: Q -&gt; Qbb | epsilon


Proof sketch

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 &gt;= 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 a or b.
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 a and bb in the terminal string. After passing that 'trapdoor', this imbalance will never be offset, since only the 'right' terminals will be produced henceforth.