Quelle  minmax_ineq.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