With version 1.15 ProB produces a warning if you use an implication inside an existential quantifier. Here we explain why.
Take a look at
f: 1..3 --> NAT & f = [0,0,0] & #i.(i:dom(f) => f(i)>0)
You may be surprised to learn that the existential quantifier on the third line is true, even though no element of the array f is greater than 0. Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as i:dom(f) is false and hence the implication is true.
Usually, one intended to write a conjunction inside the quantifier, such as the following (which is false for f=[0,0,0]</ff>):
#i.(i:dom(f) & f(i)>0)