Implication inside an Existential Quantifier

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.