How to generate a context free grammar for the language $a^i b^j c^k$ where $i+j>k$? How to generate a context free grammar for the language $a^i b^j c^k$ where $i+j>k$?
My initial thought was to find the CFG for $i+j=k$, and then go from there but I've been unable to adapt it. What I have so far is:
$$S=aSc\mid X$$
$$X=bXc\mid\varepsilon$$
 A: Maybe We should ask a different question first so we don't complicate things
How can we find a CFG for $L = \{a^ib^jc^k: i+j\geq k\}$.
Observation: For a word $L\ni w=a^ib^jc^k$ we can assign to every $c$ (from right to left) either $a$ or $b$ (from left to right). That means that we can produce that $c$ at the same time as we produced the other character (notice that there will be some characters $a,b$ with no $c$'s, meaning that you can also produce $a,b$ without producing a $c$).
Solution to $L:$
The observation allows us to easily figure out the CFG of $L$ ($S_0$ starting symbol) :
\begin{align}
S_0 &\to A \\
A &\to aA \;|\; aAc \;|\; B \\
B &\to bB \;|\; bBc \;|\; \emptyset
\end{align}
Why does this produce exactly $L$? I am not going to write the proof but I think you can work out why you can write every word $w=a^ib^jc^k$ with ($i+j\geq k)$ and it's easy to see why every word written with the grammar belongs in $L$.
If  then as you start writing $w$ if the first character you haven't written is $a$(or $b$) write you can only do $2$ operations, one wher you will also write a $c$ at the end or one where you will not
Now back to our problem, we want to find a CFG of $L_0 = \{a^ib^jc^k: i+j> k\}$.
Observation: While writing using our grammar we will do the same procedure as before but this time there must be a character $a$, $b$ with no assigned $c$. So we just need to hold this type of information, i.e if we have produced a $a$ or $b$ with no assigned $c$ so far (CFG's can do that).
Solution: We will just keep a duplicate state holding the above binary information
\begin{align}
S_0 &\to A' \\
A' &\to aA \;|\; aA'c \;|\; B' \\
A &\to aA \;|\; aAc \;|\; B \\
B' &\to bB \;|\; bB'c \\
B &\to bB \;|\; bBc \;|\; \emptyset
\end{align}
Here if $C$ is a state then $C'$ intuitively means that we have yet to produce a character $a,b$ not assigned a $c$.
Again I will skip the proof of correctness and trust that you will do it yourself.
A: We can save three states over Yuumita's answer by moving the decision on the compulsory extra $a$ or $b$ to the point where the terminal producer switches from $a$s to $b$s. This allows said decision to be put in the starting nonterminal $S$'s transitions:
$$S\to aSc\mid aS\mid aT\mid bT$$
$$T\to bTc\mid bT\mid\varepsilon$$
