| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 154 kB |
|
SSL minmax_ineq.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose : Rewrite rules to resolve inequalities involving max or min % % minmax_ineq : THEORY BEGIN a, b, c, d: VAR real min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c) min_lt : LEMMA min(a,b) < c IFF (a < c OR b < c) min_ge : LEMMA min(a,b) >= c IFF (a >= c AND b >= c) min_gt : LEMMA min(a,b) > c IFF (a > c AND b > c) le_min : LEMMA a <= min(b,c) IFF (a <= b AND a <= c) lt_min : LEMMA a < min(b,c) IFF (a < b AND a < c) ge_min : LEMMA a >= min(b,c) IFF (a >= b OR a >= c) gt_min : LEMMA a > min(b,c) IFF (a > b OR a > c) max_le : LEMMA max(a,b) <= c IFF (a <= c AND b <= c) max_lt : LEMMA max(a,b) < c IFF (a < c AND b < c) max_ge : LEMMA max(a,b) >= c IFF (a >= c OR b >= c) max_gt : LEMMA max(a,b) > c IFF (a > c OR b > c) le_max : LEMMA a <= max(b,c) IFF (a <= b OR a <= c) lt_max : LEMMA a < max(b,c) IFF (a < b OR a < c) ge_max : LEMMA a >= max(b,c) IFF (a >= b AND a >= c) gt_max : LEMMA a > max(b,c) IFF (a > b AND a > c) max_triangle: LEMMA max(a+c,b+d) <= max(a,b) + max(c,d) min_commutative: LEMMA min(a,b) = min(b,a) max_commutative: LEMMA max(a,b) = max(b,a) END minmax_ineq ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28