Find context free grammar and prove its correctness

Find context free grammar for a given language and prove its correctness:

a) $\left\{ a^ib^ja^k : i\neq j \ \vee \ j\neq k \right\}$

b) $\left\{ w\in \left\{a,b\right\}^* : \#_a(w)=2 \cdot \#_b(w) \right\}$

c) set of all words $w\in \left\{ a,b \right\}^*$ that have even length and numbers of occurrences of $b$ on even and odd positions are equal.

For a) and c) I have no idea. For b) I think I found it: $$S\rightarrow SaSaSbS \ | \ SaSbSaS \ | \ SbSaSaS \ | \ \varepsilon$$ Seems correct, but don't know how to prove that every word that has twice many $a$'s than $b$'s can be produced by this grammar. Can anybody help?

-

(a) This is the union of the languages $\left\{a^ib^ja^k:i<j\right\}$, $\left\{a^ib^ja^k:i>j\right\}$, $\left\{a^ib^ja^k:j<k\right\}$, and $\left\{a^ib^ja^k:j>k\right\}$, and it’s not too hard to write context-free grammars for these languages.
(b) Finding a proof that your grammar generates the language $L=\{w\in\{a,b\}^*:|w|_a=|w|_b\}$ seems a bit difficult, but I can do it for a somewhat different grammar. Say that $w\in L$ is irreducible if it is non-empty and not of the form $uv$ for any non-empty $u,v\in L$. Prove that if $w$ is irreducible, then there is a $u\in L$ such that $w\in\{aaub,abua,buaa\}$. Then consider the grammar with these productions:
\begin{align*} &S\to TS\mid\varepsilon\\ &T\to aaSb\mid abSa\mid bSaa \end{align*}