LTL: Show $\neg(aUb) \Leftrightarrow \neg b U (\neg a \land \neg b) \lor G \neg b$

I got as far as
\begin{align}
w \vDash \neg (a U b) &\Leftrightarrow \neg (w \vDash a U b)
\Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k < i} : w^k \vDash a) \\
&\Leftrightarrow \forall_{i\geq0} : \neg(w^i \vDash b) \lor \exists_{0\leq k < i} : \neg(w^k \vDash a)
\end{align}

but got stuck.

If you could offer some advice as on where to start I would very much appreciate it. Thanks in advance

$aUb$ means that $a$ holds up to (and not necessarily including) the first point where $b$ holds, which must exist. There are two ways in which this can fail: $b$ never holds, or the first time that $a$ fails precedes the first time in which $b$ is true. The first case is handled by $G \lnot b$. The second case is handled by $\lnot b U (\lnot a \land \lnot b)$ (why?).

StackExchange Computer Science Q#7383, answer score: 4