| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle util.pvs Sprache: PVS |
|||||||||
|
util : THEORY
BEGIN IMPORTING reals@sign, reals@sqrt b,d : VAR nnreal a,c,e : VAR real % An algebraic way to determine a*sqrt(b) = e eq(a,b,e) : bool = a*e >= 0 AND sq(a)*b = sq(e) eq_correct_1 : LEMMA eq(a,b,e) IFF a*sqrt(b) = e eq_neg : LEMMA eq(-a,b,-e) = eq(a,b,e) % An algebraic way to determine a*sqrt(b) > e gt(a,b,e) : bool = IF a >= 0 THEN e < 0 OR sq(a)*b > sq(e) ELSE e < 0 AND sq(a)*b < sq(e) ENDIF gt_correct_1 : LEMMA gt(a,b,e) IFF a*sqrt(b) > e % An algebraic way to determine a*sqrt(b) < e lt(a,b,e) : bool = gt(-a,b,-e) lt_correct_1 : LEMMA lt(a,b,e) IFF a*sqrt(b) < e % An algebraic way to determine a*sqrt(b) >= e ge(a,b,e) : bool = NOT lt(a,b,e) ge_correct_1 : LEMMA ge(a,b,e) IFF a*sqrt(b) >= e % An algebraic way to determine a*sqrt(b) <= e le(a,b,e) : bool = NOT gt(a,b,e) le_correct_1 : LEMMA le(a,b,e) IFF a*sqrt(b) <= e % An algebraic way to determine if a*sqrt(b) > c*sqrt(d)+e gt(a,b,c,d,e) : bool = IF a >= 0 THEN lt(c,d,-e) OR lt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e)) ELSE lt(c,d,-e) AND gt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e)) ENDIF gt_correct_2 : LEMMA gt(a,b,c,d,e) IFF a*sqrt(b) > c*sqrt(d)+e % An algebraic way to determine a*sqrt(b) < c*sqrt(d)+e lt(a,b,c,d,e) : bool = gt(-a,b,-c,d,-e) lt_correct_2 : LEMMA lt(a,b,c,d,e) IFF a*sqrt(b) < c*sqrt(d)+e % An algebraic way to determine a*sqrt(b) >= c*sqrt(d)+e ge(a,b,c,d,e) : bool = NOT lt(a,b,c,d,e) ge_correct_2 : LEMMA ge(a,b,c,d,e) IFF a*sqrt(b) >= c*sqrt(d)+e % An algebraic way to determine a*sqrt(b) <= c*sqrt(d)+e le(a,b,c,d,e) : bool = NOT gt(a,b,c,d,e) le_correct_2 : LEMMA le(a,b,c,d,e) IFF a*sqrt(b) <= c*sqrt(d)+e END util ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28