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