The equivalence [a SU b] = Aexists({q},1, q<->b|a&next(q), q & FG!q) is not valid: Look, for all points of time, you may have a=0, b=1 and q=1. Then, [a SU b] is always true, but this is not an accepting run of the automaton on the right hand side. Why do you think that the two formulas are equivalent?