Quantifiers bind more tightly than all operators.
Unparenthesized version Interpretation ---------------------- -------------- a < b + c Error p /\ q \/ r Error p => q => r Error x - y - z (x - y) - z a = b + c => b < s(a) (a = (b + c)) => (b < s(a)) a.b.c! ((a.b).c)! ~p /\ ~x.pre (~p) /\ (~(x.pre)) \E x (x < c) => c > 0 (\E x (x < c)) => (c > 0) \A x \E y x < y (\A x \E y x) < y