|
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
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
