Model Checking CTL* algorithm

Question

Currently I'm trying to understand the CTL* model checking algorithm from this book. The basic idea is clear to that we can use the LTL algorithm to whenever we have a subformular $E\phi$ or $A\phi$ but I have still a question I can't figure out:

Why is there no case for $\phi_1 U \phi_2$ in this algorithm? Of course we can write the until modality as a release modality but this case isn't here either. So is this algorithm incomplete or have I missed something?