affine_bandb_numerical_examples: THEORY BEGIN IMPORTING affine_bandb, affine_bandb_numerical x,y : var real example_1_a: LEMMA x<0 AND x>-5 IMPLIES x^5-2*x^3 ## [|-2875.000, 1.052|] %|- example_1_a : PROOF %|- (then (skeep) (aff-numerical (! 1 1) :precision 3 :maxdepth 9)) %|- QED example_1_b: LEMMA x<0 AND x>-1000 IMPLIES x^5-2*x^3 ## [|-999998000000000.000, 1.053|] %|- example_1_b : PROOF %|- (then (skeep) (aff-numerical (! 1 1) :precision 3 :maxdepth 16)) %|- QED example_2: LEMMA x ## [|0,10|] IMPLIES x^2 - 2*x + 1 ## [|-0.001, 81.000|] %|- example_2 : PROOF %|- (then (skeep) (aff-numerical (! 1 1) :precision 3 :maxdepth 8)) %|- QED example_legendre : LEMMA abs(x) < 1 IMPLIES 3969/65536 + 63063/4096 * x^6 + 1792791/4096 * x^10 + 3002285/4096 * x^18 + 6600165/4096 * x^14 - 72765/65536 * x^4 - 3558555/32768 * x^8 - 10207769/65536 * x^20 - 35043645/32768 * x^12 - 95851899/65536 * x^16 ## [|0.000, 0.061|] %|- example_legendre : PROOF %|- (then (skeep) (aff-numerical (! 1 1) :precision 3 :maxdepth 4)) %|- 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 example_hdp_mm: LEMMA -10 <= x0 AND x0 <= 40 AND 40 <= x1 AND x1 <= 100 AND -70 <= x2 AND x2 <= -40 AND -70 <= x3 AND x3 <= 40 AND 10 <= x4 AND x4 <= 20 AND -10 <= x5 AND x5 <= 20 AND -30 <= x6 AND x6 <= 110 AND -110 <= x7 AND x7 <= -30 IMPLIES Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [|-95100411.113, 247079452.169|] %|- example_hdp_mm : PROOF %|- (then (skeep) (aff-numerical (! 1 1) :precision 3 :maxdepth 10)) %|- QED END affine_bandb_numerical_examples