%
%
% Purpose: rewrite rules for inequalities involving floor and ceiling
%
%

floor_ceiling_ineq: THEORY


BEGIN

 a, b: VAR real
 i: VAR integer

 ge_floor_l: LEMMA floor(a) >= i IFF a >= i
 ge_floor_r: LEMMA i >= floor(a) IFF i+1 > a
 gt_floor_l: LEMMA floor(a) > i IFF a >= i+1
 gt_floor_r: LEMMA i > floor(a) IFF i > a
 le_floor_l: LEMMA floor(a) <= i IFF a < i+1
 le_floor_r: LEMMA i <= floor(a) IFF i <= a
 lt_floor_l: LEMMA floor(a) < i IFF a < i
 lt_floor_r: LEMMA i < floor(a) IFF i+1 <= a

 floor_monotone: LEMMA a <= b IMPLIES floor(a) <= floor(b)

 ge_ceiling_l: LEMMA ceiling(a) >= i IFF a > i-1
 ge_ceiling_r: LEMMA i >= ceiling(a) IFF i >= a
 gt_ceiling_l: LEMMA ceiling(a) > i IFF a > i
 gt_ceiling_r: LEMMA i > ceiling(a) IFF i-1 >= a
 le_ceiling_l: LEMMA ceiling(a) <= i IFF a <= i
 le_ceiling_r: LEMMA i <= ceiling(a) IFF i-1 < a
 lt_ceiling_l: LEMMA ceiling(a) < i IFF a <= i-1
 lt_ceiling_r: LEMMA i < ceiling(a) IFF i < a

 ceiling_monotone: LEMMA a <= b IMPLIES ceiling(a) <= ceiling(b)

END floor_ceiling_ineq