Is this language Context Free?
$L=\{a^{n+3} b^{2m} \mid n \neq m \}$
I think that I could split the languages into $L_1$ and $L_2$ with the conditions $n<m$ and $n>m$, provide 2 CF grammars and then to make the union. But I don't know how to put the condition $n<m$ to the grammar or how to think about the conditions. Thank you!
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
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 >= 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.
