%% examples4Q.pvs %% %% These examples only deal with rational expressions, for that reason the theory %% just imports strategies4Q. %%
examples4Q : theory BEGIN
IMPORTING strategies4Q
x,y : var real
%%%% Examples of numerical
zero_to_one_quarter : LEMMA
x ## [|0,1|] IMPLIES
x*(1-x) ## [|0.0000, 0.2501|] %% The expression (! 1 1) refers to formula 1, 1st term, i.e., x*(1-x) %|- zero_to_one_quarter : PROOF %|- (then (skeep) (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t)) %|- QED
x0,x1,x2,x3,x4,x5,x6,x7 : VAR real
Heart(x0,x1,x2,x3,x4,x5,x6,x7): MACRO real =
-x0*x5^3+3*x0*x5*x6^2-x2*x6^3+3*x2*x6*x5^2-x1*x4^3+3*x1*x4*x7^2-x3*x7^3+3*x3*x7*x4^2-0.9563453
hdp_mm: LEMMA
-0.1 <= x0 AND x0 <= 0.4 AND
0.4 <= x1 AND x1 <= 1 AND
-0.7 <= x2 AND x2 <= -0.4 AND
-0.7 <= x3 AND x3 <= 0.4 AND
0.1 <= x4 AND x4 <= 0.2 AND
-0.1 <= x5 AND x5 <= 0.2 AND
-0.3 <= x6 AND x6 <= 1.1 AND
-1.1 <= x7 AND x7 <= -0.3 IMPLIES
Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [|-1.852, 1.518|]
%% The expression (! 1 1) refers to formula 1, 1st term, i.e., polynomial Heart %|- hdp_mm : PROOF %|- (then (skeep) (numerical (! 1 1) :verbose? t)) %|- QED
%%%% Examples of interval
hdp_minmax: LEMMA
-0.1 <= x0 AND x0 <= 0.4 AND
0.4 <= x1 AND x1 <= 1 AND
-0.7 <= x2 AND x2 <= -0.4 AND
-0.7 <= x3 AND x3 <= 0.4 AND
0.1 <= x4 AND x4 <= 0.2 AND
-0.1 <= x5 AND x5 <= 0.2 AND
-0.3 <= x6 AND x6 <= 1.1 AND
-1.1 <= x7 AND x7 <= -0.3 IMPLIES
Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [| -1.76, 1.46 |]
%|- hdp_minmax : PROOF %|- (then (skeep) (interval)) %|- QED
common_point: LEMMA EXISTS (x,y,z:real): abs(x) <= 10 AND abs(y) <= 10 AND z ## [|0,1/2|] AND LET x2 = x^2,
y2 = y^2 IN
x2-2*x+1+y2-2*y+1<1 AND x2 + y2 < 3-2*y+0.01
%|- common_point : PROOF (interval :verbose? t) QED
Eps : posreal = 0.0001
simple_ite : LEMMA FORALL (x:real | x ## [| 0, 10 |]) : IF x <= 1 THEN sq(x) <= x+Eps ELSE sq(x) >= x-Eps ENDIF
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
