For general path formulas p and q, E(p∧q) is not equivalent to Ep∧Eq. For example, if p=Fa and q=Fb, then E(Fa∧Fb) means that we have to have one path where a holds at some time ta and b holds at some time tb. However, EFa∧EFb means that we have a path where a holds at some time ta, and we have to have a path where b holds at some time tb. The two paths in the latter case may however be two different paths which is not allowed in the former case.

If q is a state formula, however, then it holds on a path iff it holds on the first state of the path. This first state is the same first state for all paths leaving the state. Hence, we have E(p∧q) in some state s if there is path leaving where p∧q holds on that path and that means that p holds on that path and q holds in s. That is the same as (Ep)∧q and therefore E(p∧q) is equivalent in this case to (Ep)∧q.

Analogously, A(p∨q) is equivalent in this case to (Ap)∨q if q is a state formula.

Concerning your above transformation, the following are equivalent

- A!F(!E[1 WU a] & Fa)
- AG(E[1 WU a] | !Fa)
- AGA(E[1 WU a] | !Fa)
- AG(E[1 WU a] | A!Fa) (note here that E[1 WU a] is a state formula)