% % % 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
¤ 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.0.0Bemerkung:
(vorverarbeitet)
¤
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.
