Consider the $ text {CTL} ^ * $ formula $ E[pU(qUr)]$.

It is not difficult to prove that it is equivalent to $ text {CTL} $ formula $ E[pU(EqUr)]$.

The informal reason is that a road where $ p $ it's true up $ qUr $ it's true it's the same as a finite branch where $ p $ it is true along this, followed (concatenated with) by a path (which begins in a child of the last state of the previous branch) along which $ qUr $ It is true.

However, consider now $ text {CTL} ^ * $ formula $ A[pU(qUr)]$, here I have a problem in pushing the $ A $ inside, because the $ text {CTL} $ formula $ A[pU(AqUr)]$ It is "stronger" than the previous one.

The reason is that in the first one we demand that any branch contain a state from which $ qUr $ It is true. Meanwhile, the last formula requires that any branch contain a state such that **any** computing from it has $ qUr $ true.

How can I still convert $ A[pU(qUr)]$ to $ text {CTL} $?