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) &amp;\Leftrightarrow  \neg (w \vDash a U b) 
\Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k &lt; i} : w^k \vDash a)  \\
&amp;\Leftrightarrow \forall_{i\geq0} :  \neg(w^i \vDash b) \lor \exists_{0\leq k &lt; 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?).