Formally, the Phi_Inf formula is required in the ยต-calculus formulas, but one can also do without if the results are corrected afterwards in that the finally deadend states are added to all A-formulas and are removed from all E-formulas. In the example solutions we are therefore a bit sloppy with this formula. To be save, please add Phi-inf, or explain where it should be added if not written there explicitly.