% % % 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)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
