; The following example opens a PVS file called caprasse.pvs, where the formal 
; proofs of lemmas showing that, in a given region, the polynomial Caprasse
; is greater  than -3.18010 and there exists at least one point where the 
; polynomial is less than -3.18009. 

show "";
show "*** This example may take a few minutes.";
show "";

var x1 in [-0.5,0.5];
var x2 in [-0.5,0.5];
var x3 in [-0.5,0.5];
var x4 in [-0.5,0.5];
poly Caprasse = -x1*x3^3+4*x2*x3^2*x4+4*x1*x3*x4^2+2*x2*x4^3+4*x1*x3+4*x3^2-10*x2*x4-10*x4^2+2;
set precision = 0.001;
pvsfile caprasse;
check all Caprasse  >= -3.18010;
check some Caprasse <= -3.18009;
close;
exit;