# Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

Is $$GF(\psi_1 \land F\psi_2 )$$ equivalent to the property $$GF(\psi_2 \land F\psi_1 )$$?

Attempt:

In the first property each state must eventually see $$\psi_1$$ and $$\psi_2$$, in the second property as well each state must eventually see $$\psi_1$$ and $$\psi_2$$, as such the two properties must be equivalent. Is this correct?

You are right, but you should prove it. Here's a proof sketch:

Proof setup:

Suppose that $$GF(\psi_1 \land F\psi_2)$$ is true and assume towards a contradiction that $$\neg GF(F\psi_1 \land \psi_2)$$.

Observations:

Then there exists a state $$s_1$$ in which $$\neg F(F\psi_1 \land \psi_2)$$, which means that every state $$s_2 > s_1$$ has $$\neg(F\psi_1 \land \psi_2)$$, which means that for every state $$s_2$$, either $$\neg F\psi_1$$ or $$\neg \psi_2$$.

But since $$GF(\psi_1 \land F\psi_2)$$, there exists a state $$s_3 > s_2$$ such that $$s_3 \vDash \psi_1$$ and a state $$s_3 > s_2'$$ such that $$s_3' \vDash \psi_2$$, which is a contradiction.