Existential Predecessor

Question

I have a question regarding the following example:

I tried to solve it in the same way shown in the lecture video (https://es.cs.uni-kl.de/teaching/vrs/videos/VRS-04-Transitionsystems-3.html 1:08:00):

However, this does not lead to the right answer (right answer is seen above).

I also used the Tool:

I quess that one could also rephrase my question into: "Why is there no transition from the state (p,a) to itself"?

IMO there should be one since p and p' would be satiesfied and therefore (next(p)|next(q)->a&!(o->q))&p would be true.

Comments

I have the exact same problem

Answer 1

Recall the precedence rules of the propositional operators: 

Thus, disjunction binds stronger than implication.