Note that the delimiters [] are part of the binary temporal operators, so that in the formula [a SU b & EGa], the SU operator has the two arguments "a" and "b & EGa".
In general, we have the following equivalences (VRS, Chapter 7, page 45):
* [φ1 SU ψ1] ∧ [φ2 SU ψ2] ⇔ [(φ1∧φ2) SU (ψ1∧[φ2 SU ψ2] ∨ ψ2∧[φ1 SU ψ1])]
* [φ1 SU ψ1] ∧ [φ2 WU ψ2] ⇔ [(φ1∧φ2) SU (ψ1∧[φ2 WU ψ2] ∨ ψ2∧[φ1 SU ψ1])]
* [φ1 WU ψ1] ∧ [φ2 WU ψ2] ⇔ [(φ1∧φ2) WU (ψ1∧[φ2 WU ψ2] ∨ ψ2∧[φ1 WU ψ1])]
Thus, we have in particular
[a WU false] ∧ [true SU b]
⇔ [(a∧true) SU (false∧[true SU b] ∨ b∧[a WU false])]
⇔ [a SU (b∧[a WU false])]
⇔ [a SU (b∧Ga)]
Finally, E[a SU (b∧EGa)] is a CTL formula, since the path quantifiers and temporal operators occur in pairs, i.e., we have E[.SU.] and EG as the CTL operators.
