# Linear Temporal Logic, Idempotent law

in many lecture notes, I have seen the LTL idempotent law for until and its equivalence is described as $\phi U(\phi U \psi) \equiv \phi U\psi$ and also $(\phi U \psi)U\psi \equiv \phi U \psi$ . Also by definition of $G$, some formula holds in every state. So if globally $\phi$ holds until we see $\psi$ does it make every state after it true? question might sound weird but by formula is it correct to say that also $G(\phi U \psi)U\phi \equiv G(\phi U \psi)$

• Two comments: (1) the validity of an LTL formula is defined over words, not over states. (2) The last statement is ambiguous. There is no standard operator precedence for LTL, although it is typically assumed that unary operators bind stronger than binary operators. Thus, $G(\phi U \psi) U \phi$ can be read both as $(G(\phi U \psi)) U \phi$ and $G((\phi U \psi) U \phi)$, which have very different meanings. – DCTLib Jun 6 '18 at 8:30

Also by definition of $G$, some formula holds in every state.
Well, $\sf true$ holds in every state. I'm unsure about why you mention $G$ here.
So if globally $\phi$ holds until we see $\psi$ does it make every state after it true?
is it correct to say that also $G(\phi U \psi)U\phi \equiv G(\phi U \psi)$
Take $\phi = \sf false$ and $\psi = \sf true$. Then, $G(\phi U \psi)U\phi$ is equivalent to $\sf false$, and $G(\phi U \psi)$ is equivalent to $\sf true$.