| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle abs_lems.pvs Sprache: PVS |
|||||||||
|
abs_lems : THEORY
BEGIN x,y : VAR real t,a,b: VAR real z : VAR nzreal n : VAR nat IMPORTING sq,root abs_eq_0 : LEMMA abs(x) = 0 IFF x = 0 abs_0 : LEMMA abs(0) = 0 abs_nat : LEMMA abs(n) = n abs_diff : LEMMA abs(x) - abs(y) <= abs(x - y) abs_neg : LEMMA abs(-x) = abs(x) abs_diff_commute : LEMMA abs(x - y) = abs(y - x) abs_diff_0 : LEMMA x = y IFF abs(x - y) = 0 abs_add_pos : LEMMA x*y >= 0 IMPLIES abs(x+y) = abs(x)+abs(y) triangle2 : LEMMA abs(x - t) < a AND abs(x - y) < b IMPLIES abs(t - y) < a + b abs_sq : LEMMA abs(sq(a)) = sq(a) abs_lt : LEMMA abs(x) < a IFF x > -a AND x < a abs_le : LEMMA abs(x) <= a IFF x >= -a AND x <= a abs_gt : LEMMA abs(x) > a IFF x < -a OR x > a abs_ge : LEMMA abs(x) >= a IFF x <= -a OR x >= a abs_pos : LEMMA abs(x) > 0 IFF x /= 0 gt_abs : LEMMA a > abs(x) IFF x > -a AND x < a ge_abs : LEMMA a >= abs(x) IFF x >= -a AND x <= a lt_abs : LEMMA a < abs(x) IFF x < -a OR x > a le_abs : LEMMA a <= abs(x) IFF x <= -a OR x >= a pos_abs : LEMMA 0 < abs(x) IFF x /= 0 % -------- abs(f) and abs of linear function: minimum property ---- f: VAR [real -> real] m: VAR real abs_mono_inc: LEMMA m*t + b = 0 AND t <= x AND x <= y IMPLIES abs(m*x+b) <= abs(m*y+b) abs_mono_dec: LEMMA m*t + b = 0 AND x <= y AND y <= t IMPLIES abs(m*x+b) >= abs(m*y+b) AUTO_REWRITE+ abs_0 AUTO_REWRITE+ abs_nat AUTO_REWRITE- abs_diff_commute abs_root: LEMMA n>0 AND (x<0 IMPLIES odd?(n)) IMPLIES abs(root_real(x)(n)) = root_real(abs(x))(n) END abs_lems ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28