# conversion of basic $\text{CTL}^*$ formulas to $\text{CTL}$

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

It is not hard to show that it is equivalent to the $$\text{CTL}$$ formula $$E[pU(EqUr)]$$.

The informal reason is that a path where $$p$$ is true until $$qUr$$ is true is the same as a finite branch where $$p$$ is true along it, followed (concatenated with) by a path (starting at a son of the last state of the former branch) along which $$qUr$$ is true.

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

The reason is that in the former we demand that any branch contains a state starting from which $$qUr$$ is true. While, the latter formula demands that any branch contains a state such that any computation starting from it has $$qUr$$ true.

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