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