| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/examples/ (Beweissystem der NASA Version 6.0.9©) Datei vom 6.10.2014 mit Größe 2 kB |
|
Quelle sturm_tarski_examples.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28