sturm_tarski_examples : THEORY
BEGIN

  IMPORTING Tarski@strategies

  x,y : VAR real

  example_1a : LEMMA 
    x ## [|0,3|] IMPLIES x^120 -2*x^60 + 1 >= 0
%|- example_1a : PROOF
%|- (sturm)
%|- QED

  example_1b : LEMMA 
    EXISTS (x:real): x ## [|0,3|] AND x^120 -2*x^60 + 1 = 0
%|- example_1b : PROOF
%|- (sturm)
%|- QED

  example_2a : LEMMA
    x ## [|-oo,open(3)|] IMPLIES
    x^120 - (2/3)*x^60 + 1/9 >= 0
%|- example_2a : PROOF
%|- (sturm)
%|- QED

  example_2b : LEMMA
    EXISTS (x:real) : x ## [|-oo,open(3)|] AND 
                      x^120 - (2/3)*x^60 + 1/9 >= 0
%|- example_2b : PROOF
%|- (sturm)
%|- QED
                
  legendre_2(x:real) : MACRO real =
    (3*x^2-1)/2
       
  legendre_3(x:real) : MACRO real =
    (5*x^3-3*x)/2

  legendre_4(x:real) : MACRO real =
    (35*x^4-30*x^2+3)/8

  legendre_5(x:real) : MACRO real = 
    (63*x^5-70*x^3+15*x)/8
 
  legendre_6(x:real) : MACRO real =
    (231*x^6-315*x^4+105*x^2-5)/16

  legendre_8(x:real) : MACRO real =
    (6435*x^8 - 12012*x^6 + 6930*x^4 - 1260*x^2 + 35)/128

  legendre_9(x:real) : MACRO real =
    (12155*x^9 - 25740*x^7 + 18018*x^5 - 4620*x^3 + 315*x)/128

  legendre_10(x:real) : MACRO real = 
    (46189*x^10 -109395*x^8 + 90090*x^6 - 30030*x^4 + 3465*x^2 - 63)/256

  Turan_9: LEMMA
    abs(x) < 1 IMPLIES
    legendre_9(x)^2 > legendre_8(x)*legendre_10(x)
%|- Turan_9 : PROOF
%|- (sturm)
%|- QED

  Legendre_10 : LEMMA
    x ## [|-0.75,-0.6|] AND y ## [|-0.75,-0.6|] AND x < y IMPLIES
    legendre_10(x) > legendre_10(y)
%|- Legendre_10 : PROOF
%|- (mono-poly)
%|- QED

  Legendre_2_6 : LEMMA
    legendre_2(x) >= 0 OR legendre_3(x) >= 0 OR
    legendre_4(x) >= 0 OR legendre_5(x) >= 0 OR
    legendre_6(x) >= 0
%|- Legendre_2_6 : PROOF
%|- (tarski)
%|- QED

  IMPORTING vectors@vectors_2D 

  so : Vect2 = (-37040,0) % [m]
  soz: real  = 9144       % [m]^2
  vo : Vect2 = (218,218)  % [m/s]^2
  voz: real  = 2.54       % [m/s] 
  si : Vect2 = (37000,0)  % [m]^2
  siz: real  = 9000       % [m]
  vi : Vect2 = (-205,205) % [m/s]^2
  viz: real  = 2.5        % [m/s]
 
  s  : Vect2 = so-si
  sz : real  = soz-siz
  v  : Vect2 = vo-vi
  vz : real  = voz-viz

  D : real = 9260 % [m]
  H : real = 305  % [m]
  T : real = 300  % [s]

  conflict?(s,v:Vect2,T:real) : MACRO bool = 
    EXISTS (t:real | t ## [|0,T|]) : (s*s)+(2*s*v)*t+(v*v)*t^2 < sq(D) AND 
                                     abs(sz+t*vz) < H

  yes_conflict : LEMMA
    conflict?(so-si,vo-vi,300)
%|- yes_conflict : PROOF
%|- (tarski)
%|- QED

  no_conflict : LEMMA
    NOT conflict?(so-si,vo-vi,150)
%|- no_conflict : PROOF
%|- (tarski)
%|- QED

END sturm_tarski_examples