Guest examples

Below follows a few examples that guests have tried out. The second example, although valid, is not verified, as the proof-search does not duplicate the existential force quantifiers.

SPEC

variable x,y,z : int
value a,b : int
value P : int --> bool

% This is not verified 
PROPERTY : (Forall i:int. i > x) --> x=y

% Does not verify as x is first instantiated to a.
% Then the branch where P(a) is true, and P(b) is false
% does not verify.
PROPERTY : Exists x. P(x) --> P(a) /\ P(b)

% This is on the other hand verified as x can be 
% bound to a and y to b.
PROPERTY : Exists x,y. P(x) /\ P(y) --> P(a) /\ P(b)