# 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?).