Combined display of all available logs of ProB Documentation.
You can narrow down the view by selecting a log type, the username (case-sensitive), or the affected page (also case-sensitive).
06:55, 22 February 2025Michael Leuscheltalkcontribs created page Implication inside an Existential Quantifier(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...")