sturm_examples: THEORY
BEGIN

  IMPORTING Sturm@strategies

  x : VAR real

  example_1: LEMMA 
    160*((x-1/2)^2*(x-9)^4*(x+8.5)^2 + 0.1) /= 0 
%|- example_1 : PROOF
%|- (sturm)
%|- QED

  example_2: LEMMA FORALL (x:real): 
     (x-1/2)^2*(x-9)^4*(x+8.5)^2 >= 0
%|- example_2 : PROOF
%|- (sturm)
%|- QED

 example_3: LEMMA 
  (x^16-x^15-3*x^13+x^12-x^11+2*x^10-6*x^9+8*x^8 
   -7*x^7-6*x^6+5*x^5+4*x^4-3*x^3+350*x + 478)^2 /= 0
%|- example_3 : PROOF
%|- (sturm)
%|- QED

  example_4: LEMMA 
    x<0 IMPLIES x^101 < -x
%|- example_4 : PROOF
%|- (sturm)
%|- QED

  example_5: LEMMA 
    x<0 IMPLIES x^5-2*x^3 < 6
%|- example_5 : PROOF
%|- (sturm)
%|- QED

  example_6: LEMMA x^2 - 2*x + 1 >= 0
%|- example_6 : PROOF
%|- (sturm)
%|- QED

  example_7: LEMMA x*(1-x) <= 1/4
%|- example_7 : PROOF
%|- (sturm)
%|- QED


%% Examples with quantifications in antecedent and consequent

 example_8: LEMMA
   EXISTS (x:real) : x >= 0 AND x^2 - x < 0
%|- example_8 : PROOF
%|- (sturm)
%|- QED

 example_n8: LEMMA
   NOT (FORALL (x:real) : x >= 0 IMPLIES x^2 >= x)
%|- example_n8 : PROOF
%|- (sturm -1)
%|- QED

 example_80: LEMMA
   EXISTS (x:real) : x >= 0 AND x^2 - x = 0
%|- example_80 : PROOF
%|- (sturm)
%|- QED

 example_n80: LEMMA
   NOT (FORALL (x:real) : x >= 0 IMPLIES x^2 /= x)
%|- example_n80 : PROOF
%|- (sturm -1)
%|- QED

 example_9: LEMMA 
   FORALL (x:real) : x<0 IMPLIES x^5 < -x
%|- example_9 : PROOF
%|- (sturm)
%|- QED

 example_n9: LEMMA
   NOT (EXISTS (x:real): x < 0 AND x^5 >= -x)
%|- example_n9 : PROOF
%|- (sturm -1)
%|- QED

 example_90: LEMMA x<0 IMPLIES x^5 /= 0
%|- example_90 : PROOF
%|- (sturm)
%|- QED

 example_n90: LEMMA
   NOT (EXISTS (x:real): x < 0 AND x^5 = 0)
%|- example_n90 : PROOF
%|- (sturm -1)
%|- QED

  example_10 : LEMMA 
    NOT EXISTS (x:posreal) : x^3 <= 0
%|- example_10 : PROOF
%|- (sturm -1)
%|- QED

  example_11 : LEMMA
    FORALL (x:real | abs(x) <= 1) : (x-1)*(x+1) <= 0
%|- example_11 : PROOF
%|- (sturm)
%|- QED

  example_12: LEMMA
    x^120-2*x^60+1 >= 0
%|- example_12 : PROOF
%|- (sturm)
%|- QED

  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
%|- legendre : PROOF
%|- (sturm)
%|- QED

  legendre3 : 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)^3 > 0
%|- legendre3 : PROOF
%|- (sturm)
%|- QED

  harrison_sos : LEMMA
    ((x-1)^8 + 2*(x-x)^8 + (x-3)^8 -2)/4 >= 0
%|- harrison_sos : PROOF
%|- (sturm)
%|- QED

%% Examples with interval notations, including extended intervals, i.e., 
%% reals@RealInt and interval_arith@interval

  example_13 : LEMMA 
    FORALL (x:real | x ## [|-2,1|]) : x^4-x^3-19*x^2-11*x+30 <= 31.7
%|- example_13 : PROOF
%|- (sturm)
%|- QED

  example_14 : LEMMA 
    FORALL (x:real) : x ## [| 0, oo |] IMPLIES -x^3 <= 0
%|- example_14 : PROOF
%|- (sturm)
%|- QED

  example_15 : LEMMA 
    FORALL (x:real) : x ## [| open(1), oo |] IMPLIES -x^3 < 1
%|- example_15 : PROOF
%|- (sturm)
%|- QED

  example_16 : LEMMA 
    FORALL (x:real) : x ## [| -oo, 1 |] IMPLIES x*(1-x) <= 0.25
%|- example_16 : PROOF
%|- (sturm)
%|- QED

  example_17 : LEMMA
    FORALL (x:real): x>0 IMPLIES x^15*(2-x)^20*(6-x)^2*(12-x)^4*(20-x)^6>=0
%|- example_17 : PROOF
%|- (sturm)
%|- QED


% Examples of monotonicity

  mono_example_1 : LEMMA
    FORALL (x,y:real) : x >= 1 AND x < y IMPLIES (x-1/4)^2 <= y*y-(1/2)*y+(1/16)
%|- mono_example_1 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_2 : LEMMA
    FORALL (x,y:real) : x < y IMPLIES x^5 /= y^5
%|- mono_example_2 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_3: LEMMA
    FORALL (x,y:real) : 0.4 <= x AND x < y AND y <= 0.6 IMPLIES
    x^5-x^3+x/5>y*(y^4-y^2+1/5)
%|- mono_example_3 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_4: LEMMA
    FORALL (x,y:real): x /= y IMPLIES x^3 /= y^3
%|- mono_example_4 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_5: LEMMA
    EXISTS (x,y:real): x < y AND x^2 >= sq(y)
%|- mono_example_5 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_6: LEMMA
    EXISTS (x:real,y:real|y>=-1): x > y AND x^4 < y^4
%|- mono_example_6 : PROOF
%|- (mono-poly)
%|- QED

 END sturm_examples