(Created page with " 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 <pre> f: 1..3 --> NAT & f = [0,0,0] & #i.(i:dom(f) => f(i)>0) </pre> 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 <tt>i:dom(f)</tt> is false and hence the imp...") |
No edit summary |
||
| Line 12: | Line 12: | ||
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. | 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 <tt>i:dom(f)</tt> is false and hence the implication is true. | Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> 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 <tt>f=[0,0,0]</ff>): | |||
<pre> | |||
#i.(i:dom(f) & f(i)>0) | |||
</pre> | |||
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)