# LTL Until Tautology

Today I had to prove some tautologies as an exercise, one of them was:

(Ga)->(Fb) equivalent aU(b v ¬a)

It is clear that I have to prove the implication in both ways. After putting into negation normal form i get that:

F(¬a v b) -> aU(b v ¬a) and viceversa.

I managed to prove the opposite implication, since aU(b v ¬a) implies that at some point we will either see b or ¬a, but I couldn't get around proving the other direction. I am sure it is because we have a and ¬a on the opposing sites of U, but the reasoning is not clear to me.

Can someone clear this up for me?

Let us try to prove that $F(\neg a \vee b) \rightarrow a\,\mathcal{U}\,(b \vee \neg a)$ is a tautology. For this, we have to show that every word that is a model of $F(\neg a \vee b)$ is also a model of $a\,\mathcal{U}\,(b \vee \neg a)$
Let $i \in \mathbb{N}$ be the least index of the word for which we have $w^i \models (\neg a \vee b)$, where $w^i$ denotes taking a word $w_0 w_1 w_2 \ldots$ and removing all letters up to $w_{i-1}$. By the assumption that $w \models F(\neg a \vee b)$, we know that such an index exists, so we can pick the least such index. Because $i$ is the least such index, we know that for all $0 \leq j < i$, we have $w^j \not\models (\neg a \vee b)$, and hence $w^j \models a \wedge \neg b$ and also also $w^j \models a$.
So we know that $w^i \models (\neg a \vee b)$ and for all $0 \leq j<i$, we have $w^j \models a$. By the definition of the until operator, we thus have $w \models a\,\mathcal{U}\,(\neg a \vee b)$.