elementary-bounders

Included Books

other

(in-package "ACL2")

local

(local (include-book "arithmetic-5/top" :dir :system))

local

(local (deftheory jared-disables
    '(|(equal (if a b c) x)| |(equal x (if a b c))|
      |(+ x (if a b c))|
      simplify-products-gather-exponents-<
      (:t expt-type-prescription-integerp-base)
      (:t expt-type-prescription-integerp-base-a)
      (:t expt-type-prescription-nonpositive-base-odd-exponent)
      (:t expt-type-prescription-nonpositive-base-even-exponent)
      (:t expt-type-prescription-negative-base-odd-exponent)
      (:t expt-type-prescription-negative-base-even-exponent)
      (:t expt-type-prescription-integerp-base-b)
      (:t expt-type-prescription-rationalp-base)
      (:t expt-type-prescription-non-0-base)
      (:t not-integerp-3b)
      (:t not-integerp-1b)
      (:t not-integerp-2b)
      (:t not-integerp-4e)
      (:t not-integerp-4b)
      (:t not-integerp-4b-expt)
      (:t not-integerp-3b-expt)
      (:t not-integerp-2b-expt)
      (:t not-integerp-1b-expt)
      (:t rationalp-expt-type-prescription)
      rationalp-x
      acl2-numberp-x
      not-integerp-1a
      not-integerp-2a
      not-integerp-3a
      not-integerp-4a
      not-integerp-1d
      not-integerp-2d
      not-integerp-3d
      not-integerp-4d
      not-integerp-1f
      not-integerp-2f
      not-integerp-3f
      not-integerp-4f
      default-times-1
      default-times-2
      default-less-than-1
      default-less-than-2
      default-car
      default-cdr)))

local

(local (in-theory (disable jared-disables)))

local

(local (set-default-hints '((nonlinearp-default-hint++ id
       stable-under-simplificationp
       hist
       nil) (and stable-under-simplificationp
        (not (cw "Jared-hint: re-enabling slow rules.~%"))
        '(:in-theory (enable jared-disables))))))

local

(local (defthm abstract-def-<?
    (implies (implies (and x y)
        (or (real/rationalp x) (real/rationalp y)))
      (iff (<? rel x y)
        (if (or (null x) (null y))
          t
          (if rel
            (< x y)
            (<= x y)))))
    :hints (("Goal" :use ((:instance completion-of-< (x x) (y y)) (:instance completion-of-< (x y) (y x)))))
    :rule-classes ((:rewrite :corollary (implies (real/rationalp x)
         (iff (<? rel x y)
           (if (or (null x) (null y))
             t
             (if rel
               (< x y)
               (<= x y)))))) (:rewrite :corollary (implies (real/rationalp y)
          (iff (<? rel x y)
            (if (or (null x) (null y))
              t
              (if rel
                (< x y)
                (<= x y))))))
      (:rewrite :corollary (implies (null x)
          (iff (<? rel x y)
            (if (or (null x) (null y))
              t
              (if rel
                (< x y)
                (<= x y))))))
      (:rewrite :corollary (implies (null y)
          (iff (<? rel x y)
            (if (or (null x) (null y))
              t
              (if rel
                (< x y)
                (<= x y)))))))))

local

(local (in-theory (disable <?)))

local

(local (defthm interval-accessors
    (and (equal (tau-interval-dom (make-tau-interval dom lo-rel lo hi-rel hi))
        dom)
      (equal (tau-interval-lo-rel (make-tau-interval dom lo-rel lo hi-rel hi))
        lo-rel)
      (equal (tau-interval-lo (make-tau-interval dom lo-rel lo hi-rel hi))
        lo)
      (equal (tau-interval-hi-rel (make-tau-interval dom lo-rel lo hi-rel hi))
        hi-rel)
      (equal (tau-interval-hi (make-tau-interval dom lo-rel lo hi-rel hi))
        hi))))

local

(local (defthm intervalp-rules
    (implies (tau-intervalp int)
      (and (implies (equal (tau-interval-dom int) 'integerp)
          (and (equal (tau-interval-lo-rel int) nil)
            (equal (tau-interval-hi-rel int) nil)
            (equal (integerp (tau-interval-lo int))
              (if (tau-interval-lo int)
                t
                nil))
            (equal (integerp (tau-interval-hi int))
              (if (tau-interval-hi int)
                t
                nil))))
        (booleanp (tau-interval-lo-rel int))
        (booleanp (tau-interval-hi-rel int))
        (equal (rationalp (tau-interval-lo int))
          (if (tau-interval-lo int)
            t
            nil))
        (equal (rationalp (tau-interval-hi int))
          (if (tau-interval-hi int)
            t
            nil))
        (implies (and (tau-interval-lo int) (tau-interval-hi int))
          (<= (tau-interval-lo int) (tau-interval-hi int)))))
    :rule-classes ((:rewrite :corollary (implies (tau-intervalp int)
         (and (equal (rationalp (tau-interval-lo int))
             (if (tau-interval-lo int)
               t
               nil))
           (equal (rationalp (tau-interval-hi int))
             (if (tau-interval-hi int)
               t
               nil))))) (:rewrite :corollary (implies (and (equal (tau-interval-dom int) 'integerp)
            (tau-intervalp int))
          (and (equal (tau-interval-lo-rel int) nil)
            (equal (tau-interval-hi-rel int) nil)
            (equal (integerp (tau-interval-lo int))
              (if (tau-interval-lo int)
                t
                nil))
            (equal (integerp (tau-interval-hi int))
              (if (tau-interval-hi int)
                t
                nil)))))
      (:forward-chaining :corollary (implies (and (tau-intervalp int)
            (equal (tau-interval-dom int) 'integerp)
            (tau-interval-lo int))
          (integerp (tau-interval-lo int))))
      (:forward-chaining :corollary (implies (and (tau-intervalp int)
            (equal (tau-interval-dom int) 'integerp)
            (tau-interval-hi int))
          (integerp (tau-interval-hi int))))
      (:forward-chaining :corollary (implies (and (tau-intervalp int) (tau-interval-lo int))
          (rationalp (tau-interval-lo int))))
      (:forward-chaining :corollary (implies (and (tau-intervalp int) (tau-interval-hi int))
          (rationalp (tau-interval-hi int))))
      (:linear :corollary (implies (and (tau-intervalp int)
            (tau-interval-lo int)
            (tau-interval-hi int))
          (<= (tau-interval-lo int) (tau-interval-hi int)))))))

local

(local (defthm in-tau-intervalp-rules
    (and (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          (eq (tau-interval-dom int) 'integerp))
        (integerp x))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          (eq (tau-interval-dom int) 'rationalp))
        (rationalp x))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          (eq (tau-interval-dom int) 'acl2-numberp))
        (acl2-numberp x))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          x
          (tau-interval-lo-rel int)
          (tau-interval-lo int))
        (< (tau-interval-lo int) x))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          x
          (not (tau-interval-lo-rel int))
          (tau-interval-lo int))
        (<= (tau-interval-lo int) x))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          x
          (tau-interval-hi-rel int)
          (tau-interval-hi int))
        (< x (tau-interval-hi int)))
      (implies (and (tau-intervalp int)
          (in-tau-intervalp x int)
          (not (tau-interval-hi-rel int))
          x
          (tau-interval-hi int))
        (<= x (tau-interval-hi int))))
    :rule-classes ((:forward-chaining :corollary (implies (and (in-tau-intervalp x int)
           (tau-intervalp int)
           (eq (tau-interval-dom int) 'integerp))
         (integerp x))) (:forward-chaining :corollary (implies (and (in-tau-intervalp x int)
            (tau-intervalp int)
            (eq (tau-interval-dom int) 'rationalp))
          (rationalp x)))
      (:forward-chaining :corollary (implies (and (in-tau-intervalp x int)
            (tau-intervalp int)
            (eq (tau-interval-dom int) 'acl2-numberp))
          (acl2-numberp x)))
      (:linear :corollary (implies (and (in-tau-intervalp x int)
            x
            (tau-intervalp int)
            (tau-interval-lo-rel int)
            (tau-interval-lo int))
          (< (tau-interval-lo int) x)))
      (:linear :corollary (implies (and (in-tau-intervalp x int)
            x
            (tau-intervalp int)
            (tau-interval-lo int))
          (<= (tau-interval-lo int) x)))
      (:linear :corollary (implies (and (in-tau-intervalp x int)
            x
            (tau-intervalp int)
            (tau-interval-hi-rel int)
            (tau-interval-hi int))
          (< x (tau-interval-hi int))))
      (:linear :corollary (implies (and (in-tau-intervalp x int)
            x
            (tau-intervalp int)
            (tau-interval-hi int))
          (<= x (tau-interval-hi int)))))))

local

(local (defthm intervalp-make-tau-interval
    (equal (tau-intervalp (make-tau-interval dom lo-rel lo hi-rel hi))
      (cond ((eq dom 'integerp) (and (null lo-rel)
            (null hi-rel)
            (if lo
              (and (integerp lo)
                (if hi
                  (and (integerp hi) (<= lo hi))
                  t))
              (if hi
                (integerp hi)
                t))))
        (t (and (member dom '(rationalp acl2-numberp nil))
            (booleanp lo-rel)
            (booleanp hi-rel)
            (if lo
              (and (rationalp lo)
                (if hi
                  (and (rationalp hi) (<= lo hi))
                  t))
              (if hi
                (rationalp hi)
                t))))))))

local

(local (defthm in-tau-intervalp-make-tau-interval
    (equal (in-tau-intervalp x
        (make-tau-interval dom lo-rel lo hi-rel hi))
      (and (tau-interval-domainp dom x)
        (<? lo-rel lo (fix x))
        (<? hi-rel (fix x) hi)))))

local

(local (in-theory (disable make-tau-interval
      tau-interval-dom
      tau-interval-lo-rel
      tau-interval-lo
      tau-interval-hi-rel
      tau-interval-hi)))

domain-of-binary-arithmetic-functionfunction

(defun domain-of-binary-arithmetic-function
  (domx domy)
  (declare (xargs :guard (and (symbolp domx) (symbolp domy))))
  (cond ((eq domx 'integerp) (cond ((eq domy 'integerp) 'integerp)
        ((eq domy 'rationalp) 'rationalp)
        (t 'acl2-numberp)))
    ((eq domx 'rationalp) (cond ((or (eq domy 'integerp) (eq domy 'rationalp)) 'rationalp)
        (t 'acl2-numberp)))
    (t 'acl2-numberp)))

bounds-of-sumfunction

(defun bounds-of-sum
  (lo-rel1 lo1 hi-rel1 hi1 lo-rel2 lo2 hi-rel2 hi2)
  (declare (xargs :guard (and (booleanp lo-rel1)
        (or (null lo1) (rationalp lo1))
        (booleanp hi-rel1)
        (or (null hi1) (rationalp hi1))
        (booleanp lo-rel2)
        (or (null lo2) (rationalp lo2))
        (booleanp hi-rel2)
        (or (null hi2) (rationalp hi2)))))
  (mv-let (lo-rel lo)
    (if (and lo1 lo2)
      (mv (or lo-rel1 lo-rel2) (+ lo1 lo2))
      (mv nil nil))
    (mv-let (hi-rel hi)
      (if (and hi1 hi2)
        (mv (or hi-rel1 hi-rel2) (+ hi1 hi2))
        (mv nil nil))
      (mv lo-rel lo hi-rel hi))))

tau-bounder-+function

(defun tau-bounder-+
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1) (tau-intervalp int2))))
  (let ((dom (domain-of-binary-arithmetic-function (tau-interval-dom int1)
         (tau-interval-dom int2))))
    (mv-let (lo-rel lo hi-rel hi)
      (bounds-of-sum (tau-interval-lo-rel int1)
        (tau-interval-lo int1)
        (tau-interval-hi-rel int1)
        (tau-interval-hi int1)
        (tau-interval-lo-rel int2)
        (tau-interval-lo int2)
        (tau-interval-hi-rel int2)
        (tau-interval-hi int2))
      (make-tau-interval dom lo-rel lo hi-rel hi))))

tau-bounder-+-correcttheorem

(defthm tau-bounder-+-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-+ int1 int2))
      (in-tau-intervalp (+ x y) (tau-bounder-+ int1 int2))))
  :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (and (tau-intervalp (tau-bounder-+ int1 int2))
          (in-tau-intervalp (+ x y) (tau-bounder-+ int1 int2))))
      :trigger-terms ((tau-bounder-+ int1 int2)))))

extended-rationalpfunction

(defund extended-rationalp
  (x)
  (declare (xargs :guard t))
  (or (equal x nil) (equal x t) (real/rationalp x)))

local

(local (defthm |extended-rationalp is rationalp when not nil or t|
    (implies (and (extended-rationalp x)
        (not (equal x nil))
        (not (equal x t)))
      (real/rationalp x))
    :hints (("Goal" :in-theory (enable extended-rationalp)))))

local

(local (defthm |rationalp is extended-rationalp|
    (implies (real/rationalp x) (extended-rationalp x))
    :hints (("Goal" :in-theory (enable extended-rationalp)))))

local

(local (defthm |rationalp when acl2-numberp and extended-rationalp|
    (implies (and (acl2-numberp x) (extended-rationalp x))
      (real/rationalp x))))

bounds-of-product-<function

(defun bounds-of-product-<
  (x y)
  (declare (xargs :guard (and (extended-rationalp x) (extended-rationalp y))))
  (if (null x)
    t
    (if (eq x t)
      (if (eq y t)
        t
        nil)
      (if (null y)
        nil
        (if (eq y t)
          t
          (< x y))))))

bounds-of-product-<=function

(defun bounds-of-product-<=
  (x y)
  (declare (xargs :guard (and (extended-rationalp x) (extended-rationalp y))))
  (if (null x)
    t
    (if (eq x t)
      (if (eq y t)
        t
        nil)
      (if (null y)
        nil
        (if (eq y t)
          t
          (<= x y))))))

bounds-of-product-*function

(defun bounds-of-product-*
  (x y)
  (declare (xargs :guard (and (extended-rationalp x) (extended-rationalp y))))
  (if (or (eql x 0) (eql y 0))
    0
    (if (or (null x) (eq x t) (null y) (eq y t))
      (let ((signx (cond ((null x) nil) ((eq x t) t) ((< x 0) nil) (t t))) (signy (cond ((null y) nil) ((eq y t) t) ((< y 0) nil) (t t))))
        (eq signx signy))
      (* x y))))

bounds-of-product1function

(defun bounds-of-product1
  (lo-rel1 lo1 hi-rel1 hi1 lo-rel2 lo2 hi-rel2 hi2)
  (declare (xargs :guard (and (booleanp lo-rel1)
        (extended-rationalp lo1)
        (booleanp hi-rel1)
        (extended-rationalp hi1)
        (booleanp lo-rel2)
        (extended-rationalp lo2)
        (booleanp hi-rel2)
        (extended-rationalp hi2))))
  (cond ((equal lo1 hi1) (cond ((bounds-of-product-< 0 lo1) (mv lo-rel2
            (bounds-of-product-* lo1 lo2)
            hi-rel2
            (bounds-of-product-* lo1 hi2)))
        ((equal lo1 0) (mv nil 0 nil 0))
        (t (mv hi-rel2
            (bounds-of-product-* lo1 hi2)
            lo-rel2
            (bounds-of-product-* lo1 lo2)))))
    ((equal lo2 hi2) (cond ((bounds-of-product-< 0 lo2) (mv lo-rel1
            (bounds-of-product-* lo1 lo2)
            hi-rel1
            (bounds-of-product-* hi1 hi2)))
        ((equal lo2 0) (mv nil 0 nil 0))
        (t (mv hi-rel1
            (bounds-of-product-* hi1 lo2)
            lo-rel1
            (bounds-of-product-* lo1 lo2)))))
    ((and (bounds-of-product-<= 0 lo1)
       (bounds-of-product-<= 0 lo2)) (mv (and (or lo-rel1 lo-rel2)
          (or lo-rel1 (not (equal lo1 0)))
          (or lo-rel2 (not (equal lo2 0))))
        (bounds-of-product-* lo1 lo2)
        (or hi-rel1 hi-rel2)
        (bounds-of-product-* hi1 hi2)))
    ((and (bounds-of-product-<= hi1 0)
       (bounds-of-product-<= hi2 0)) (mv (and (or hi-rel1 hi-rel2)
          (or hi-rel1 (not (equal hi1 0)))
          (or hi-rel2 (not (equal hi2 0))))
        (bounds-of-product-* hi1 hi2)
        (or lo-rel1 lo-rel2)
        (bounds-of-product-* lo1 lo2)))
    ((and (bounds-of-product-<= 0 lo1)
       (bounds-of-product-<= hi2 0)) (mv (or hi-rel1 lo-rel2)
        (bounds-of-product-* hi1 lo2)
        (and (or lo-rel1 hi-rel2)
          (or lo-rel1 (not (equal lo1 0)))
          (or hi-rel2 (not (equal hi2 0))))
        (bounds-of-product-* lo1 hi2)))
    ((and (bounds-of-product-<= hi1 0)
       (bounds-of-product-<= 0 lo2)) (mv (or lo-rel1 hi-rel2)
        (bounds-of-product-* lo1 hi2)
        (and (or hi-rel1 lo-rel2)
          (or hi-rel1 (not (equal hi1 0)))
          (or lo-rel2 (not (equal lo2 0))))
        (bounds-of-product-* hi1 lo2)))
    ((and (bounds-of-product-< lo1 0)
       (bounds-of-product-< 0 hi1)
       (bounds-of-product-<= 0 lo2)) (mv (or lo-rel1 hi-rel2)
        (bounds-of-product-* lo1 hi2)
        (or hi-rel1 hi-rel2)
        (bounds-of-product-* hi1 hi2)))
    ((and (bounds-of-product-< lo1 0)
       (bounds-of-product-< 0 hi1)
       (bounds-of-product-<= hi2 0)) (mv (or hi-rel1 lo-rel2)
        (bounds-of-product-* hi1 lo2)
        (or lo-rel1 lo-rel2)
        (bounds-of-product-* lo1 lo2)))
    ((and (bounds-of-product-<= 0 lo1)
       (bounds-of-product-< lo2 0)
       (bounds-of-product-< 0 hi2)) (mv (or hi-rel1 lo-rel2)
        (bounds-of-product-* hi1 lo2)
        (or hi-rel1 hi-rel2)
        (bounds-of-product-* hi1 hi2)))
    ((and (bounds-of-product-<= hi1 0)
       (bounds-of-product-< lo2 0)
       (bounds-of-product-< 0 hi2)) (mv (or lo-rel1 hi-rel2)
        (bounds-of-product-* lo1 hi2)
        (or lo-rel1 lo-rel2)
        (bounds-of-product-* lo1 lo2)))
    (t (cond ((and (bounds-of-product-< (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (bounds-of-product-< (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (or lo-rel1 hi-rel2)
            (bounds-of-product-* lo1 hi2)
            (or hi-rel1 hi-rel2)
            (bounds-of-product-* hi1 hi2)))
        ((and (bounds-of-product-< (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (equal (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (or lo-rel1 hi-rel2)
            (bounds-of-product-* lo1 hi2)
            (and (or lo-rel1 lo-rel2) (or hi-rel1 hi-rel2))
            (bounds-of-product-* lo1 lo2)))
        ((and (bounds-of-product-< (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (bounds-of-product-< (bounds-of-product-* hi1 hi2)
             (bounds-of-product-* lo1 lo2))) (mv (or lo-rel1 hi-rel2)
            (bounds-of-product-* lo1 hi2)
            (or lo-rel1 lo-rel2)
            (bounds-of-product-* lo1 lo2)))
        ((and (equal (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (bounds-of-product-< (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (and (or lo-rel1 hi-rel2) (or hi-rel1 lo-rel2))
            (bounds-of-product-* lo1 hi2)
            (or hi-rel1 hi-rel2)
            (bounds-of-product-* hi1 hi2)))
        ((and (equal (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (equal (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (and (or lo-rel1 hi-rel2) (or hi-rel1 lo-rel2))
            (bounds-of-product-* lo1 hi2)
            (and (or lo-rel1 lo-rel2) (or hi-rel1 hi-rel2))
            (bounds-of-product-* lo1 lo2)))
        ((and (equal (bounds-of-product-* lo1 hi2)
             (bounds-of-product-* hi1 lo2))
           (bounds-of-product-< (bounds-of-product-* hi1 hi2)
             (bounds-of-product-* lo1 lo2))) (mv (and (or lo-rel1 hi-rel2) (or hi-rel1 lo-rel2))
            (bounds-of-product-* lo1 hi2)
            (or lo-rel1 lo-rel2)
            (bounds-of-product-* lo1 lo2)))
        ((and (bounds-of-product-< (bounds-of-product-* hi1 lo2)
             (bounds-of-product-* lo1 hi2))
           (bounds-of-product-< (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (or hi-rel1 lo-rel2)
            (bounds-of-product-* hi1 lo2)
            (or hi-rel1 hi-rel2)
            (bounds-of-product-* hi1 hi2)))
        ((and (bounds-of-product-< (bounds-of-product-* hi1 lo2)
             (bounds-of-product-* lo1 hi2))
           (equal (bounds-of-product-* lo1 lo2)
             (bounds-of-product-* hi1 hi2))) (mv (or hi-rel1 lo-rel2)
            (bounds-of-product-* hi1 lo2)
            (and (or lo-rel1 lo-rel2) (or hi-rel1 hi-rel2))
            (bounds-of-product-* lo1 lo2)))
        (t (mv (or hi-rel1 lo-rel2)
            (bounds-of-product-* hi1 lo2)
            (or lo-rel1 lo-rel2)
            (bounds-of-product-* lo1 lo2)))))))

bounds-of-productfunction

(defun bounds-of-product
  (lo-rel1 lo1 hi-rel1 hi1 lo-rel2 lo2 hi-rel2 hi2)
  (declare (xargs :guard (and (booleanp lo-rel1)
        (or (null lo1) (real/rationalp lo1))
        (booleanp hi-rel1)
        (or (null hi1) (real/rationalp hi1))
        (booleanp lo-rel2)
        (or (null lo2) (real/rationalp lo2))
        (booleanp hi-rel2)
        (or (null hi2) (real/rationalp hi2)))))
  (let ((hi1 (if (null hi1)
         t
         hi1)) (hi2 (if (null hi2)
          t
          hi2)))
    (mv-let (lo-rel lo hi-rel hi)
      (bounds-of-product1 lo-rel1
        lo1
        hi-rel1
        hi1
        lo-rel2
        lo2
        hi-rel2
        hi2)
      (mv (if (null lo)
          nil
          lo-rel)
        lo
        (if (eq hi t)
          nil
          hi-rel)
        (if (eq hi t)
          nil
          hi)))))

tau-bounder-*function

(defun tau-bounder-*
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1) (tau-intervalp int2))))
  (let ((dom (domain-of-binary-arithmetic-function (tau-interval-dom int1)
         (tau-interval-dom int2))))
    (mv-let (lo-rel lo hi-rel hi)
      (bounds-of-product (tau-interval-lo-rel int1)
        (tau-interval-lo int1)
        (tau-interval-hi-rel int1)
        (tau-interval-hi int1)
        (tau-interval-lo-rel int2)
        (tau-interval-lo int2)
        (tau-interval-hi-rel int2)
        (tau-interval-hi int2))
      (make-tau-interval dom lo-rel lo hi-rel hi))))

local

(local (defthm |tau-intervalp tau-bounder-*|
    (implies (and (tau-intervalp int1) (tau-intervalp int2))
      (tau-intervalp (tau-bounder-* int1 int2)))))

local

(local (defthm |tau-interval-dom tau-bounder-*|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (or (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int1) 'rationalp))
        (or (equal (tau-interval-dom int2) 'integerp)
          (equal (tau-interval-dom int2) 'rationalp))
        (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
            'integerp)))
      (equal (tau-interval-dom (tau-bounder-* int1 int2))
        'rationalp))
    :hints (("Goal" :in-theory (disable bounds-of-product)))))

local

(local (encapsulate nil
    (local (in-theory (disable the-floor-below
          the-floor-above
          reduce-rational-multiplicative-constant-<
          reduce-multiplicative-constant-<
          reduce-additive-constant-<
          integerp-<-constant
          constant-<-integerp
          remove-strict-inequalities
          remove-weak-inequalities
          prefer-positive-addends-<
          |(< c (/ x)) positive c --- present in goal|
          |(< c (/ x)) positive c --- obj t or nil|
          |(< c (/ x)) negative c --- present in goal|
          |(< c (/ x)) negative c --- obj t or nil|
          |(< c (- x))|
          |(< (/ x) c) positive c --- present in goal|
          |(< (/ x) c) positive c --- obj t or nil|
          |(< (/ x) c) negative c --- present in goal|
          |(< (/ x) c) negative c --- obj t or nil|
          |(< (/ x) (/ y))|
          |(< (- x) c)|
          |(< (- x) (- y))|
          intervalp-rules
          reduce-rationalp-+
          reduce-rationalp-*
          rationalp-minus-x
          meta-rationalp-correct
          simplify-products-gather-exponents-equal
          reduce-multiplicative-constant-equal
          reduce-additive-constant-equal
          prefer-positive-addends-equal
          equal-of-predicates-rewrite
          |(equal c (/ x))|
          |(equal c (- x))|
          |(equal (/ x) c)|
          |(equal (/ x) (/ y))|
          |(equal (- x) c)|
          |(equal (- x) (- y))|
          |(< (/ x) 0)|
          |(< (* x y) 0)|
          (:type-prescription in-tau-intervalp)
          (:type-prescription tau-intervalp)
          (:type-prescription tau-interval-domainp)
          normalize-factors-gather-exponents
          simplify-terms-such-as-ax+bx-<-0-rational-remainder
          simplify-terms-such-as-ax+bx-<-0-rational-common
          simplify-sums-equal
          |(< 0 (/ x))|
          |(< 0 (* x y))|
          integerp-minus-x
          (:type-prescription booleanp)
          |(< 0 (* x y)) rationalp (* x y)|
          meta-integerp-correct
          default-plus-1
          default-plus-2
          default-divide
          member)))
    (local (set-default-hints '((and stable-under-simplificationp '(:nonlinearp t)) (and stable-under-simplificationp
            (not (cw "Jared-hint: re-enabling slow rules.~%"))
            '(:in-theory (enable jared-disables)))
          (and stable-under-simplificationp
            (not (cw "Jared-hint: splitting into cases.~%"))
            '(:cases ((and (< 0 x) (< 0 y)) (and (< 0 x) (equal 0 y))
                (and (< 0 x) (< y 0))
                (and (equal 0 x) (< 0 y))
                (and (equal 0 x) (equal 0 y))
                (and (equal 0 x) (< y 0))
                (and (< x 0) (< 0 y))
                (and (< x 0) (equal 0 y))
                (and (< x 0) (< y 0)))))
          (and stable-under-simplificationp
            (nonlinearp-default-hint++ id
              stable-under-simplificationp
              hist
              nil)))))
    (defthm |in-tau-intervalp tau-bounder-*|
      (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (or (equal (tau-interval-dom int1) 'integerp)
            (equal (tau-interval-dom int1) 'rationalp))
          (or (equal (tau-interval-dom int2) 'integerp)
            (equal (tau-interval-dom int2) 'rationalp))
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))))))

tau-bounder-*-correctencapsulate

(encapsulate nil
  (local (in-theory (disable tau-bounder-*)))
  (defthm tau-bounder-*-correct
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (or (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int1) 'rationalp))
        (or (equal (tau-interval-dom int2) 'integerp)
          (equal (tau-interval-dom int2) 'rationalp))
        (in-tau-intervalp x int1)
        (in-tau-intervalp y int2))
      (and (tau-intervalp (tau-bounder-* int1 int2))
        (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))
        (implies (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
              'integerp))
          (equal (tau-interval-dom (tau-bounder-* int1 int2))
            'rationalp))))
    :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'integerp)
            (equal (tau-interval-dom int2) 'integerp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-* int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-* int1 int2))
                'rationalp))
            (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))))
        :trigger-terms ((tau-bounder-* int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'integerp)
            (equal (tau-interval-dom int2) 'rationalp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-* int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-* int1 int2))
                'rationalp))
            (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))))
        :trigger-terms ((tau-bounder-* int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'rationalp)
            (equal (tau-interval-dom int2) 'integerp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-* int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-* int1 int2))
                'rationalp))
            (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))))
        :trigger-terms ((tau-bounder-* int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'rationalp)
            (equal (tau-interval-dom int2) 'rationalp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-* int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-* int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-* int1 int2))
                'rationalp))
            (in-tau-intervalp (* x y) (tau-bounder-* int1 int2))))
        :trigger-terms ((tau-bounder-* int1 int2))))))

*tau-interval-for--1*constant

(defconst *tau-interval-for--1*
  (make-tau-interval 'integerp nil -1 nil -1))

tau-bounder--function

(defun tau-bounder--
  (int)
  (declare (xargs :guard (tau-intervalp int)))
  (tau-bounder-* *tau-interval-for--1* int))

tau-bounder---correcttheorem

(defthm tau-bounder---correct
  (implies (and (tau-intervalp int1)
      (or (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int1) 'rationalp))
      (in-tau-intervalp x int1))
    (and (tau-intervalp (tau-bounder-- int1))
      (in-tau-intervalp (unary-- x) (tau-bounder-- int1))
      (implies (not (equal (tau-interval-dom (tau-bounder-- int1)) 'integerp))
        (equal (tau-interval-dom (tau-bounder-- int1)) 'rationalp))))
  :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (equal (tau-interval-dom int1) 'integerp)
          (in-tau-intervalp x int1))
        (and (tau-intervalp (tau-bounder-- int1))
          (in-tau-intervalp (unary-- x) (tau-bounder-- int1))
          (equal (tau-interval-dom (tau-bounder-- int1)) 'integerp)))
      :trigger-terms ((tau-bounder-- int1)))
    (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (equal (tau-interval-dom int1) 'rationalp)
          (in-tau-intervalp x int1))
        (and (tau-intervalp (tau-bounder-- int1))
          (in-tau-intervalp (unary-- x) (tau-bounder-- int1))
          (equal (tau-interval-dom (tau-bounder-- int1)) 'rationalp)))
      :trigger-terms ((tau-bounder-* int1 int2)))))

bounds-of-reciprocalfunction

(defun bounds-of-reciprocal
  (x dom lo-rel lo hi-rel hi)
  (declare (ignore x))
  (declare (xargs :guard (and (symbolp dom)
        (booleanp lo-rel)
        (or (null lo) (real/rationalp lo))
        (booleanp hi-rel)
        (or (null hi) (real/rationalp hi))
        (or (null lo) (null hi) (<= lo hi)))))
  (let ((-oo (if (eq dom 'integerp)
         -1
         nil)) (+oo (if (eq dom 'integerp)
          1
          nil)))
    (cond ((null lo) (cond ((null hi) (mv nil -oo nil +oo))
          ((< hi 0) (mv hi-rel (/ hi) t 0))
          ((equal hi 0) (mv nil -oo hi-rel 0))
          (t (mv nil -oo nil +oo))))
      ((< 0 lo) (cond ((null hi) (mv t 0 lo-rel (/ lo)))
          (t (mv hi-rel (/ hi) lo-rel (/ lo)))))
      ((equal 0 lo) (cond ((null hi) (mv lo-rel 0 nil +oo))
          ((equal 0 hi) (mv nil 0 nil 0))
          (lo-rel (mv hi-rel (/ hi) nil +oo))
          (t (mv nil 0 nil +oo))))
      ((or (null hi) (< 0 hi)) (mv nil -oo nil +oo))
      ((equal 0 hi) (cond (hi-rel (mv nil -oo lo-rel (/ lo)))
          (t (mv nil -oo nil 0))))
      (t (mv hi-rel (/ hi) lo-rel (/ lo))))))

tau-bounder-/function

(defun tau-bounder-/
  (int)
  (declare (xargs :guard (tau-intervalp int)))
  (mv-let (lo-rel lo hi-rel hi)
    (bounds-of-reciprocal 0
      (tau-interval-dom int)
      (tau-interval-lo-rel int)
      (tau-interval-lo int)
      (tau-interval-hi-rel int)
      (tau-interval-hi int))
    (make-tau-interval 'rationalp lo-rel lo hi-rel hi)))

local

(local (defthm |tau-intervalp tau-bounder-/|
    (implies (tau-intervalp int1)
      (tau-intervalp (tau-bounder-/ int1)))))

local

(local (defthm |tau-interval-dom tau-bounder-/|
    (equal (tau-interval-dom (tau-bounder-/ int1)) 'rationalp)
    :hints (("Goal" :in-theory (disable bounds-of-reciprocal)))))

local

(local (defthm |in-tau-intervalp tau-bounder-/|
    (implies (and (tau-intervalp int1)
        (or (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int1) 'rationalp))
        (in-tau-intervalp x int1))
      (in-tau-intervalp (/ x) (tau-bounder-/ int1)))))

tau-bounder-/-correcttheorem

(defthm tau-bounder-/-correct
  (implies (and (tau-intervalp int1)
      (or (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int1) 'rationalp))
      (in-tau-intervalp x int1))
    (and (tau-intervalp (tau-bounder-/ int1))
      (in-tau-intervalp (/ x) (tau-bounder-/ int1))
      (equal (tau-interval-dom (tau-bounder-/ int1)) 'rationalp)))
  :hints (("Goal" :in-theory (disable tau-bounder-/)))
  :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (equal (tau-interval-dom int1) 'integerp)
          (in-tau-intervalp x int1))
        (and (tau-intervalp (tau-bounder-/ int1))
          (equal (tau-interval-dom (tau-bounder-/ int1)) 'rationalp)
          (in-tau-intervalp (/ x) (tau-bounder-/ int1))))
      :trigger-terms ((tau-bounder-/ int1)))
    (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (equal (tau-interval-dom int1) 'rationalp)
          (in-tau-intervalp x int1))
        (and (tau-intervalp (tau-bounder-/ int1))
          (equal (tau-interval-dom (tau-bounder-/ int1)) 'rationalp)
          (in-tau-intervalp (/ x) (tau-bounder-/ int1))))
      :trigger-terms ((tau-bounder-/ int1)))))

local

(local (defthm floor-tau-bounder-domain (integerp (floor x y))))

tau-bounder-floorfunction

(defun tau-bounder-floor
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1) (tau-intervalp int2))
      :guard-hints (("Goal" :cases ((tau-intervalp (tau-bounder-* int1 (tau-bounder-/ int2))))
         :in-theory (disable tau-bounder-* tau-bounder-/)) ("Subgoal 2" :use ((:instance |tau-intervalp tau-bounder-*|
             (int1 int1)
             (int2 (tau-bounder-/ int2))) (:instance |tau-intervalp tau-bounder-/| (int1 int2)))))))
  (let ((int (tau-bounder-* int1 (tau-bounder-/ int2))))
    (make-tau-interval 'integerp
      nil
      (if (tau-interval-lo int)
        (floor (tau-interval-lo int) 1)
        nil)
      nil
      (if (tau-interval-hi int)
        (floor (tau-interval-hi int) 1)
        nil))))

tau-bounder-floor-correcttheorem

(defthm tau-bounder-floor-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (or (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int1) 'rationalp))
      (or (equal (tau-interval-dom int2) 'integerp)
        (equal (tau-interval-dom int2) 'rationalp))
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-floor int1 int2))
      (in-tau-intervalp (floor x y) (tau-bounder-floor int1 int2))
      (equal (tau-interval-dom (tau-bounder-floor int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (disable tau-intervalp
       in-tau-intervalp
       tau-bounder-*
       tau-bounder-/
       (:executable-counterpart make-tau-interval))))
  :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int2) 'integerp)
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (and (tau-intervalp (tau-bounder-floor int1 int2))
          (equal (tau-interval-dom (tau-bounder-floor int1 int2))
            'integerp)
          (in-tau-intervalp (floor x y) (tau-bounder-floor int1 int2))))
      :trigger-terms ((tau-bounder-floor int1 int2)))
    (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int2) 'rationalp)
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (and (tau-intervalp (tau-bounder-floor int1 int2))
          (equal (tau-interval-dom (tau-bounder-floor int1 int2))
            'integerp)
          (in-tau-intervalp (floor x y) (tau-bounder-floor int1 int2))))
      :trigger-terms ((tau-bounder-floor int1 int2)))
    (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (equal (tau-interval-dom int1) 'rationalp)
          (equal (tau-interval-dom int2) 'integerp)
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (and (tau-intervalp (tau-bounder-floor int1 int2))
          (equal (tau-interval-dom (tau-bounder-floor int1 int2))
            'integerp)
          (in-tau-intervalp (floor x y) (tau-bounder-floor int1 int2))))
      :trigger-terms ((tau-bounder-floor int1 int2)))
    (:forward-chaining :corollary (implies (and (tau-intervalp int1)
          (tau-intervalp int2)
          (equal (tau-interval-dom int1) 'rationalp)
          (equal (tau-interval-dom int2) 'rationalp)
          (in-tau-intervalp x int1)
          (in-tau-intervalp y int2))
        (and (tau-intervalp (tau-bounder-floor int1 int2))
          (equal (tau-interval-dom (tau-bounder-floor int1 int2))
            'integerp)
          (in-tau-intervalp (floor x y) (tau-bounder-floor int1 int2))))
      :trigger-terms ((tau-bounder-floor int1 int2)))))

lower-bound->function

(defun lower-bound->
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    nil
    (if (null b)
      t
      (if (and a-rel (not b-rel))
        (>= a b)
        (> a b)))))

upper-bound-<function

(defun upper-bound-<
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    nil
    (if (null b)
      t
      (if (and a-rel (not b-rel))
        (<= a b)
        (< a b)))))

combine-intervals1function

(defun combine-intervals1
  (dom1 lo-rel1 lo1 hi-rel1 hi1 dom2 lo-rel2 lo2 hi-rel2 hi2)
  (declare (xargs :guard (and (symbolp dom1)
        (booleanp lo-rel1)
        (or (null lo1) (rationalp lo1))
        (booleanp hi-rel1)
        (or (null hi1) (rationalp hi1))
        (symbolp dom2)
        (booleanp lo-rel2)
        (or (null lo2) (rationalp lo2))
        (booleanp hi-rel2)
        (or (null hi2) (rationalp hi2)))))
  (mv-let (lo-rel lo)
    (if (lower-bound-> lo-rel1 lo1 lo-rel2 lo2)
      (mv lo-rel2 lo2)
      (mv lo-rel1 lo1))
    (mv-let (hi-rel hi)
      (if (upper-bound-< hi-rel1 hi1 hi-rel2 hi2)
        (mv hi-rel2 hi2)
        (mv hi-rel1 hi1))
      (make-tau-interval (domain-of-binary-arithmetic-function dom1 dom2)
        lo-rel
        lo
        hi-rel
        hi))))

squeeze-kfunction

(defun squeeze-k
  (upper-boundp rel k)
  (declare (xargs :guard (and (booleanp upper-boundp)
        (booleanp rel)
        (or (null k) (rationalp k)))))
  (if k
    (if (integerp k)
      (if rel
        (if upper-boundp
          (- k 1)
          (+ k 1))
        k)
      (if upper-boundp
        (floor k 1)
        (ceiling k 1)))
    nil))

make-tau-interval-with-integerp-fixfunction

(defun make-tau-interval-with-integerp-fix
  (dom lo-rel lo hi-rel hi)
  (declare (xargs :guard (and (symbolp dom)
        (booleanp lo-rel)
        (or (null lo) (rationalp lo))
        (booleanp hi-rel)
        (or (null hi) (rationalp hi)))))
  (cond ((eq dom 'integerp) (cond ((and (null lo-rel)
           (or (null lo) (integerp lo))
           (null hi-rel)
           (or (null hi) (integerp hi))) (make-tau-interval 'integerp nil lo nil hi))
        (t (let ((lo (squeeze-k nil lo-rel lo)) (hi (squeeze-k t hi-rel hi)))
            (make-tau-interval 'integerp nil lo nil hi)))))
    (t (make-tau-interval dom lo-rel lo hi-rel hi))))

tau-bounder-modfunction

(defun tau-bounder-mod
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1) (tau-intervalp int2))))
  (let ((domx (tau-interval-dom int1)) (lo-relx (tau-interval-lo-rel int1))
      (lox (tau-interval-lo int1))
      (hi-relx (tau-interval-hi-rel int1))
      (hix (tau-interval-hi int1))
      (domy (tau-interval-dom int2))
      (lo-rely (tau-interval-lo-rel int2))
      (loy (tau-interval-lo int2))
      (hi-rely (tau-interval-hi-rel int2))
      (hiy (tau-interval-hi int2)))
    (cond ((and (rationalp loy)
         (if lo-rely
           (<= 0 loy)
           (< 0 loy))) (make-tau-interval-with-integerp-fix (domain-of-binary-arithmetic-function domx domy)
          nil
          0
          t
          hiy))
      ((and (rationalp hiy)
         (if hi-rely
           (<= hiy 0)
           (< hiy 0))) (make-tau-interval-with-integerp-fix (domain-of-binary-arithmetic-function domx domy)
          t
          loy
          nil
          0))
      (t (combine-intervals1 domx
          lo-relx
          lox
          hi-relx
          hix
          domy
          lo-rely
          loy
          hi-rely
          hiy)))))

tau-bounder-mod-correctencapsulate

(encapsulate nil
  (local (in-theory (disable jared-disables)))
  (local (in-theory (disable (:t not-integerp-4b)
        (:t not-integerp-3b)
        (:t not-integerp-2b)
        (:t not-integerp-1b)
        mod-nonnegative
        mod-nonpositive
        mod-zero
        mod-positive
        mod-negative
        mod-x-y-=-x
        mod-x-y-=-x+y
        mod-x-y-=-x-y
        the-floor-below
        the-floor-above
        default-times-1
        default-times-2
        default-plus-1
        default-plus-2
        reduce-rational-multiplicative-constant-<
        |(< c (/ x)) positive c --- present in goal|
        |(< c (/ x)) positive c --- obj t or nil|
        |(< c (/ x)) negative c --- present in goal|
        |(< c (/ x)) negative c --- obj t or nil|
        |(< c (- x))|
        |(< (/ x) c) positive c --- present in goal|
        |(< (/ x) c) positive c --- obj t or nil|
        |(< (/ x) c) negative c --- present in goal|
        |(< (/ x) c) negative c --- obj t or nil|
        |(< (/ x) (/ y))|
        |(< (- x) c)|
        |(< (- x) (- y))|
        rationalp-x
        prefer-positive-exponents-scatter-exponents-<-2
        prefer-positive-exponents-scatter-exponents-equal
        default-car
        default-cdr
        cancel-mod-+
        meta-integerp-correct
        meta-rationalp-correct
        acl2-numberp-x
        in-tau-intervalp-rules
        intervalp-rules)))
  (local (set-default-hints '((and stable-under-simplificationp '(:nonlinearp t)) (and stable-under-simplificationp
          (nonlinearp-default-hint++ id
            stable-under-simplificationp
            hist
            nil))
        (and stable-under-simplificationp
          (not (cw "Jared-hint: re-enabling slower rules.~%"))
          '(:in-theory (enable jared-disables))))))
  (defthm tau-bounder-mod-correct
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (or (equal (tau-interval-dom int1) 'integerp)
          (equal (tau-interval-dom int1) 'rationalp))
        (or (equal (tau-interval-dom int2) 'integerp)
          (equal (tau-interval-dom int2) 'rationalp))
        (in-tau-intervalp x int1)
        (in-tau-intervalp y int2))
      (and (tau-intervalp (tau-bounder-mod int1 int2))
        (in-tau-intervalp (mod x y) (tau-bounder-mod int1 int2))
        (implies (not (equal (tau-interval-dom (tau-bounder-mod int1 int2))
              'integerp))
          (equal (tau-interval-dom (tau-bounder-mod int1 int2))
            'rationalp))))
    :rule-classes ((:rewrite) (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'integerp)
            (equal (tau-interval-dom int2) 'integerp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-mod int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                'rationalp))
            (in-tau-intervalp (mod x y) (tau-bounder-mod int1 int2))))
        :trigger-terms ((tau-bounder-mod int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'integerp)
            (equal (tau-interval-dom int2) 'rationalp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-mod int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                'rationalp))
            (in-tau-intervalp (mod x y) (tau-bounder-mod int1 int2))))
        :trigger-terms ((tau-bounder-mod int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'rational)
            (equal (tau-interval-dom int2) 'integerp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-mod int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                'rationalp))
            (in-tau-intervalp (mod x y) (tau-bounder-mod int1 int2))))
        :trigger-terms ((tau-bounder-mod int1 int2)))
      (:forward-chaining :corollary (implies (and (tau-intervalp int1)
            (tau-intervalp int2)
            (equal (tau-interval-dom int1) 'rationalp)
            (equal (tau-interval-dom int2) 'rationalp)
            (in-tau-intervalp x int1)
            (in-tau-intervalp y int2))
          (and (tau-intervalp (tau-bounder-mod int1 int2))
            (implies (not (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                  'integerp))
              (equal (tau-interval-dom (tau-bounder-mod int1 int2))
                'rationalp))
            (in-tau-intervalp (mod x y) (tau-bounder-mod int1 int2))))
        :trigger-terms ((tau-bounder-mod int1 int2))))))

local

(local (defthm logand-tau-bounder-both-nonnegative
    (implies (and (<= 0 minx)
        (<= minx x)
        (<= x maxx)
        (<= 0 miny)
        (<= miny y)
        (<= y maxy))
      (and (<= 0 (logand x y)) (<= (logand x y) (min maxx maxy))))
    :rule-classes (:rewrite :linear)))

shifts-to-all-onesfunction

(defun shifts-to-all-ones
  (x)
  (declare (xargs :guard (integerp x)))
  (if (and (integerp x) (< x 0))
    (if (equal x -1)
      0
      (+ 1 (shifts-to-all-ones (ash x -1))))
    0))

local

(local (encapsulate nil
    (local (defthm expt-2-shifts-to-all-ones
        (implies (and (integerp x) (< x 0))
          (<= (- (expt 2 (shifts-to-all-ones x))) x))
        :rule-classes :linear))
    (local (defthm logand-both-negative-lower-bound
        (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
          (<= (- (expt 2 (max (shifts-to-all-ones x) (shifts-to-all-ones y))))
            (logand x y)))
        :hints (("Goal" :in-theory (e/d (logand) (|(logand (floor x 2) (floor y 2))|))))
        :rule-classes nil))
    (local (defthm logand-both-negative
        (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
          (and (<= (- (expt 2 (max (shifts-to-all-ones x) (shifts-to-all-ones y))))
              (logand x y))
            (<= (logand x y) (min x y))))
        :hints (("Goal" :use logand-both-negative-lower-bound))
        :rule-classes nil))
    (local (defun shifts-to-all-ones-monotonic-hint
        (x y)
        (if (and (integerp x) (< x 0) (integerp y) (< y 0))
          (if (equal x -1)
            0
            (if (equal y -1)
              0
              (shifts-to-all-ones-monotonic-hint (ash x -1) (ash y -1))))
          0)))
    (local (defthm shifts-to-all-ones-monotic
        (implies (and (integerp x) (integerp y) (< y 0) (<= x y))
          (<= (shifts-to-all-ones y) (shifts-to-all-ones x)))
        :hints (("Goal" :induct (shifts-to-all-ones-monotonic-hint x y)))
        :rule-classes nil))
    (defthm logand-tau-bounder-both-negative
      (implies (and (integerp x)
          (integerp y)
          (integerp minx)
          (integerp miny)
          (integerp maxx)
          (integerp maxy)
          (<= minx x)
          (<= x maxx)
          (< maxx 0)
          (<= miny y)
          (<= y maxy)
          (< maxy 0))
        (and (<= (- (expt 2
                (max (shifts-to-all-ones minx) (shifts-to-all-ones miny))))
            (logand x y))
          (<= (logand x y) (min maxx maxy))))
      :hints (("Goal" :use ((:instance logand-both-negative) (:instance shifts-to-all-ones-monotic (x minx) (y x))
           (:instance shifts-to-all-ones-monotic (x miny) (y y)))))
      :rule-classes (:rewrite :linear))))

local

(local (defthm logand-tau-bounder-both-either-lower-bound
    (implies (and (integerp x)
        (integerp y)
        (integerp minx)
        (integerp miny)
        (<= minx x)
        (<= miny y))
      (<= (min 0
          (- (expt 2
              (max (shifts-to-all-ones minx) (shifts-to-all-ones miny)))))
        (logand x y)))
    :hints (("Goal" :in-theory (disable max)
       :cases ((and (< x 0) (< y 0)))))
    :rule-classes (:rewrite :linear)))

local

(local (defthm logand-tau-bounder-both-either-upper-bound
    (implies (and (integerp x) (integerp y) (<= x maxx) (<= y maxy))
      (<= (logand x y) (max maxx maxy)))
    :hints (("Goal" :cases ((and (< x 0) (< y 0)))))
    :rule-classes (:rewrite :linear)))

local

(local (include-book "find-minimal-2d"))

find-minimal-logand2function

(defun find-minimal-logand2
  (x loy hiy min)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hiy)) (ifix loy)))
      :guard (and (integerp x)
        (integerp loy)
        (integerp hiy)
        (or (null min) (integerp min)))
      :verify-guards nil))
  (cond ((mbe :logic (not (and (integerp loy) (integerp hiy)))
       :exec nil) min)
    ((> loy hiy) min)
    (t (find-minimal-logand2 x
        (+ 1 loy)
        hiy
        (if (or (null min) (< (logand x loy) min))
          (logand x loy)
          min)))))

find-minimal-logand1function

(defun find-minimal-logand1
  (lox hix loy hiy min)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hix)) (ifix lox)))
      :guard (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy)
        (or (null min) (integerp min)))
      :verify-guards nil))
  (cond ((mbe :logic (not (and (integerp lox) (integerp hix)))
       :exec nil) min)
    ((> lox hix) min)
    (t (find-minimal-logand1 (+ 1 lox)
        hix
        loy
        hiy
        (find-minimal-logand2 lox loy hiy min)))))

find-minimal-logandfunction

(defun find-minimal-logand
  (lox hix loy hiy)
  (declare (xargs :guard (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy))
      :verify-guards nil))
  (find-minimal-logand1 lox hix loy hiy nil))

local

(local (defthm find-minimal-logand-correct
    (implies (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy)
        (integerp x)
        (<= lox x)
        (<= x hix)
        (integerp y)
        (<= loy y)
        (<= y hiy))
      (and (integerp (find-minimal-logand lox hix loy hiy))
        (<= (find-minimal-logand lox hix loy hiy) (logand x y))))
    :hints (("Goal" :use (:functional-instance find-minimal-correct
         (fmla (lambda (x y) (logand x y)))
         (find-minimal2 find-minimal-logand2)
         (find-minimal1 find-minimal-logand1)
         (find-minimal find-minimal-logand))))))

in-theory

(in-theory (disable find-minimal-logand))

local

(local (include-book "find-maximal-2d"))

find-maximal-logand2function

(defun find-maximal-logand2
  (x loy hiy max)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hiy)) (ifix loy)))
      :guard (and (integerp x)
        (integerp loy)
        (integerp hiy)
        (or (null max) (integerp max)))
      :verify-guards nil))
  (cond ((mbe :logic (not (and (integerp loy) (integerp hiy)))
       :exec nil) max)
    ((> loy hiy) max)
    (t (find-maximal-logand2 x
        (+ 1 loy)
        hiy
        (if (or (null max) (> (logand x loy) max))
          (logand x loy)
          max)))))

find-maximal-logand1function

(defun find-maximal-logand1
  (lox hix loy hiy max)
  (declare (xargs :measure (nfix (- (+ 1 (ifix hix)) (ifix lox)))
      :guard (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy)
        (or (null max) (integerp max)))
      :verify-guards nil))
  (cond ((mbe :logic (not (and (integerp lox) (integerp hix)))
       :exec nil) max)
    ((> lox hix) max)
    (t (find-maximal-logand1 (+ 1 lox)
        hix
        loy
        hiy
        (find-maximal-logand2 lox loy hiy max)))))

find-maximal-logandfunction

(defun find-maximal-logand
  (lox hix loy hiy)
  (declare (xargs :guard (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy))
      :verify-guards nil))
  (find-maximal-logand1 lox hix loy hiy nil))

other

(verify-guards find-minimal-logand2)

other

(verify-guards find-minimal-logand1)

other

(verify-guards find-minimal-logand)

other

(verify-guards find-maximal-logand2)

other

(verify-guards find-maximal-logand1)

other

(verify-guards find-maximal-logand)

local

(local (defthm find-maximal-logand-correct
    (implies (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy)
        (integerp x)
        (<= lox x)
        (<= x hix)
        (integerp y)
        (<= loy y)
        (<= y hiy))
      (and (integerp (find-maximal-logand lox hix loy hiy))
        (>= (find-maximal-logand lox hix loy hiy) (logand x y))))
    :hints (("Goal" :use (:functional-instance find-maximal-correct
         (fmla (lambda (x y) (logand x y)))
         (find-maximal2 find-maximal-logand2)
         (find-maximal1 find-maximal-logand1)
         (find-maximal find-maximal-logand))))))

in-theory

(in-theory (disable find-maximal-logand))

find-minimal-logand-below-find-maximal-logandtheorem

(defthm find-minimal-logand-below-find-maximal-logand
  (implies (and (integerp lox)
      (integerp hix)
      (integerp loy)
      (integerp hiy)
      (<= lox hix)
      (<= loy hiy))
    (<= (find-minimal-logand lox hix loy hiy)
      (find-maximal-logand lox hix loy hiy)))
  :hints (("Goal" :use ((:instance find-minimal-logand-correct (x lox) (y loy)) (:instance find-maximal-logand-correct (x lox) (y loy)))
     :in-theory (disable find-minimal-logand-correct
       find-maximal-logand-correct)))
  :rule-classes :linear)

*logand-empirical-threshhold*constant

(defconst *logand-empirical-threshhold* (* 1024 1024))

worth-computingpfunction

(defun worth-computingp
  (lox hix loy hiy)
  (declare (xargs :guard (and (integerp lox)
        (integerp hix)
        (integerp loy)
        (integerp hiy))))
  (< (* (if (<= lox hix)
        (+ 1 (- hix lox))
        0)
      (if (<= loy hiy)
        (+ 1 (- hiy loy))
        0))
    *logand-empirical-threshhold*))

in-theory

(in-theory (disable worth-computingp))

tau-bounder-logandfunction

(defun tau-bounder-logand
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))))
  (let ((lox (tau-interval-lo int1)) (hix (tau-interval-hi int1))
      (loy (tau-interval-lo int2))
      (hiy (tau-interval-hi int2)))
    (cond ((and lox hix loy hiy (worth-computingp lox hix loy hiy)) (make-tau-interval 'integerp
          nil
          (find-minimal-logand lox hix loy hiy)
          nil
          (find-maximal-logand lox hix loy hiy)))
      ((and lox (<= 0 lox) loy (<= 0 loy)) (make-tau-interval 'integerp
          nil
          0
          nil
          (and hix hiy (min hix hiy))))
      ((and hix (< hix 0) hiy (< hiy 0)) (make-tau-interval 'integerp
          nil
          (and lox
            loy
            (- (expt 2
                (max (shifts-to-all-ones lox) (shifts-to-all-ones loy)))))
          nil
          (min hix hiy)))
      ((and hix (<= hix 0) loy (<= 0 loy)) (make-tau-interval 'integerp nil 0 nil hiy))
      ((and hiy (<= hiy 0) lox (<= 0 lox)) (make-tau-interval 'integerp nil 0 nil hix))
      ((and lox (<= 0 lox)) (make-tau-interval 'integerp
          nil
          0
          nil
          (and hix hiy (max hix hiy))))
      ((and loy (<= 0 loy)) (make-tau-interval 'integerp
          nil
          0
          nil
          (and hix hiy (max hix hiy))))
      (t (make-tau-interval 'integerp
          nil
          (and lox
            loy
            (min 0
              (- (expt 2
                  (max (shifts-to-all-ones lox) (shifts-to-all-ones loy))))))
          nil
          (and hix hiy (max hix hiy)))))))

local

(local (defthm min-max-properties
    (and (<= (min x y) x)
      (<= (min x y) y)
      (<= x (max x y))
      (<= y (max x y)))
    :rule-classes :linear))

local

(local (defthm |tau-intervalp tau-bounder-logand|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      (tau-intervalp (tau-bounder-logand int1 int2)))
    :hints (("Goal" :in-theory (disable min max)))))

local

(local (defthm |tau-interval-dom tau-bounder-logand|
    (equal (tau-interval-dom (tau-bounder-logand int1 int2))
      'integerp)))

local

(local (defthm |in-tau-intervalp tau-bounder-logand|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp)
        (in-tau-intervalp x int1)
        (in-tau-intervalp y int2))
      (in-tau-intervalp (logand x y)
        (tau-bounder-logand int1 int2)))
    :hints (("Goal" :in-theory (disable min max)))))

tau-bounder-logand-correcttheorem

(defthm tau-bounder-logand-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-logand int1 int2))
      (in-tau-intervalp (logand x y)
        (tau-bounder-logand int1 int2))
      (equal (tau-interval-dom (tau-bounder-logand int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (disable tau-bounder-logand)))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-logand int1 int2)))))

tau-bounder-lognotfunction

(defun tau-bounder-lognot
  (int)
  (declare (xargs :guard (tau-intervalp int)))
  (let ((lo (tau-interval-lo int)) (hi (tau-interval-hi int)))
    (make-tau-interval 'integerp
      nil
      (if hi
        (- (- hi) 1)
        nil)
      nil
      (if lo
        (- (- lo) 1)
        nil))))

local

(local (defthm |tau-intervalp tau-bounder-lognot|
    (implies (and (tau-intervalp int)
        (equal (tau-interval-dom int) 'integerp))
      (and (tau-intervalp (tau-bounder-lognot int))
        (equal (tau-interval-dom (tau-bounder-lognot int))
          'integerp)))
    :hints (("Goal" :in-theory (disable min max)))))

tau-bounder-lognot-correcttheorem

(defthm tau-bounder-lognot-correct
  (implies (and (tau-intervalp int1)
      (equal (tau-interval-dom int1) 'integerp)
      (in-tau-intervalp x int1))
    (and (tau-intervalp (tau-bounder-lognot int1))
      (in-tau-intervalp (lognot x) (tau-bounder-lognot int1))
      (equal (tau-interval-dom (tau-bounder-lognot int1))
        'integerp)))
  :hints (("Goal" :in-theory (enable lognot)))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-lognot int1)))))

tau-bounder-logiorfunction

(defun tau-bounder-logior
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (equal (tau-interval-dom int1) 'integerp)
        (tau-intervalp int2)
        (equal (tau-interval-dom int2) 'integerp))
      :guard-hints (("Goal" :use ((:instance |tau-intervalp tau-bounder-lognot|
            (int (tau-bounder-logand (tau-bounder-lognot int1)
                (tau-bounder-lognot int2)))) (:instance |tau-intervalp tau-bounder-logand|
             (int1 (tau-bounder-lognot int1))
             (int2 (tau-bounder-lognot int2)))
           (:instance |tau-intervalp tau-bounder-lognot| (int int1))
           (:instance |tau-intervalp tau-bounder-lognot| (int int2)))
         :in-theory (disable tau-intervalp
           tau-bounder-lognot
           tau-bounder-logand)))))
  (tau-bounder-lognot (tau-bounder-logand (tau-bounder-lognot int1)
      (tau-bounder-lognot int2))))

local

(local (defthm |tau-intervalp tau-bounder-logior|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      (and (tau-intervalp (tau-bounder-logior int1 int2))
        (equal (tau-interval-dom (tau-bounder-logior int1 int2))
          'integerp)))
    :hints (("Goal" :in-theory (e/d (logior)
         (tau-intervalp in-tau-intervalp
           tau-bounder-logand
           tau-bounder-lognot
           lognot-logand
           (:executable-counterpart make-tau-interval)))))))

tau-bounder-logior-correcttheorem

(defthm tau-bounder-logior-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-logior int1 int2))
      (in-tau-intervalp (logior x y)
        (tau-bounder-logior int1 int2))
      (equal (tau-interval-dom (tau-bounder-logior int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (e/d (logior)
       (tau-intervalp in-tau-intervalp
         tau-bounder-logand
         tau-bounder-lognot
         lognot-logand
         (:executable-counterpart make-tau-interval)))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-logior int1 int2)))))

tau-bounder-logorc1function

(defun tau-bounder-logorc1
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (equal (tau-interval-dom int1) 'integerp)
        (tau-intervalp int2)
        (equal (tau-interval-dom int2) 'integerp))
      :guard-hints (("Goal" :use ((:instance |tau-intervalp tau-bounder-logior|
            (int1 (tau-bounder-lognot int1))
            (int2 int2)) (:instance |tau-intervalp tau-bounder-lognot| (int int1)))
         :in-theory (disable tau-intervalp
           tau-bounder-logior
           tau-bounder-lognot)))))
  (tau-bounder-logior (tau-bounder-lognot int1) int2))

local

(local (defthm |tau-intervalp tau-bounder-logorc1|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      (and (tau-intervalp (tau-bounder-logorc1 int1 int2))
        (equal (tau-interval-dom (tau-bounder-logorc1 int1 int2))
          'integerp)))
    :hints (("Goal" :in-theory (e/d (logorc1)
         (tau-intervalp in-tau-intervalp
           tau-bounder-logand
           tau-bounder-lognot
           |(logior y x)|
           (:executable-counterpart make-tau-interval)))))))

tau-bounder-logorc1-correcttheorem

(defthm tau-bounder-logorc1-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-logorc1 int1 int2))
      (in-tau-intervalp (logorc1 x y)
        (tau-bounder-logorc1 int1 int2))
      (equal (tau-interval-dom (tau-bounder-logorc1 int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (e/d (logorc1)
       (tau-intervalp in-tau-intervalp
         tau-bounder-logior
         tau-bounder-lognot
         |(logior y x)|
         (:executable-counterpart make-tau-interval)))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-logorc1 int1 int2)))))

tau-bounder-logeqvfunction

(defun tau-bounder-logeqv
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      :guard-hints (("Goal" :use ((:instance |tau-intervalp tau-bounder-logand|
            (int1 (tau-bounder-logorc1 int1 int2))
            (int2 (tau-bounder-logorc1 int2 int1))) (:instance |tau-intervalp tau-bounder-logorc1|
             (int1 int1)
             (int2 int2))
           (:instance |tau-intervalp tau-bounder-logorc1|
             (int1 int2)
             (int2 int1)))
         :in-theory (disable tau-intervalp
           tau-bounder-logand
           tau-bounder-logorc1)))))
  (tau-bounder-logand (tau-bounder-logorc1 int1 int2)
    (tau-bounder-logorc1 int2 int1)))

local

(local (defthm |tau-intervalp tau-bounder-logeqv|
    (implies (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      (and (tau-intervalp (tau-bounder-logeqv int1 int2))
        (equal (tau-interval-dom (tau-bounder-logeqv int1 int2))
          'integerp)))
    :hints (("Goal" :in-theory (e/d (logeqv)
         (tau-intervalp in-tau-intervalp
           tau-bounder-logand
           tau-bounder-logorc1
           (:executable-counterpart make-tau-interval)))))))

tau-bounder-logeqv-correcttheorem

(defthm tau-bounder-logeqv-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-logeqv int1 int2))
      (in-tau-intervalp (logeqv x y)
        (tau-bounder-logeqv int1 int2))
      (equal (tau-interval-dom (tau-bounder-logeqv int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (e/d (logeqv)
       (tau-intervalp in-tau-intervalp
         logorc1
         tau-bounder-logand
         tau-bounder-logorc1
         (:executable-counterpart make-tau-interval)))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-logeqv int1 int2)))))

tau-bounder-logxorfunction

(defun tau-bounder-logxor
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))
      :guard-hints (("Goal" :use ((:instance |tau-intervalp tau-bounder-lognot|
            (int (tau-bounder-logeqv int1 int2))) (:instance |tau-intervalp tau-bounder-logeqv|
             (int1 int1)
             (int2 int2)))
         :in-theory (disable tau-intervalp
           tau-bounder-lognot
           tau-bounder-logeqv)))))
  (tau-bounder-lognot (tau-bounder-logeqv int1 int2)))

tau-bounder-logxor-correcttheorem

(defthm tau-bounder-logxor-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-logxor int1 int2))
      (in-tau-intervalp (logxor x y)
        (tau-bounder-logxor int1 int2))
      (equal (tau-interval-dom (tau-bounder-logxor int1 int2))
        'integerp)))
  :hints (("Goal" :in-theory (e/d (logxor)
       (tau-intervalp in-tau-intervalp
         logeqv
         tau-bounder-lognot
         tau-bounder-logeqv
         (:executable-counterpart make-tau-interval)))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-logxor int1 int2)))))

tau-bounder-expt2function

(defun tau-bounder-expt2
  (int2)
  (declare (xargs :guard (and (tau-intervalp int2)
        (equal (tau-interval-dom int2) 'integerp))))
  (let ((loy (tau-interval-lo int2)) (hiy (tau-interval-hi int2)))
    (if loy
      (if (<= 0 loy)
        (if hiy
          (make-tau-interval 'integerp
            nil
            (expt 2 loy)
            nil
            (expt 2 hiy))
          (make-tau-interval 'integerp nil (expt 2 loy) nil nil))
        (if hiy
          (make-tau-interval 'rationalp
            nil
            (expt 2 loy)
            nil
            (expt 2 hiy))
          (make-tau-interval 'rationalp nil (expt 2 loy) nil nil)))
      (if hiy
        (make-tau-interval 'rationalp t 0 nil (expt 2 hiy))
        (make-tau-interval 'rationalp t 0 nil nil)))))

tau-bounder-expt2-correcttheorem

(defthm tau-bounder-expt2-correct
  (implies (and (tau-intervalp int2)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-expt2 int2))
      (in-tau-intervalp (expt 2 y) (tau-bounder-expt2 int2))
      (implies (not (equal (tau-interval-dom (tau-bounder-expt2 int2))
            'integerp))
        (equal (tau-interval-dom (tau-bounder-expt2 int2))
          'rationalp))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-expt2 int2)))))

tau-bounder-exptfunction

(defun tau-bounder-expt
  (intr inti)
  (declare (xargs :guard (and (tau-intervalp intr)
        (tau-intervalp inti)
        (equal (tau-interval-dom intr) 'integerp)
        (equal (tau-interval-dom inti) 'integerp))))
  (if (and (equal (tau-interval-lo intr) 2)
      (equal (tau-interval-hi intr) 2))
    (tau-bounder-expt2 inti)
    (make-tau-interval 'rationalp nil nil nil nil)))

tau-bounder-expt-correcttheorem

(defthm tau-bounder-expt-correct
  (implies (and (tau-intervalp intr)
      (equal (tau-interval-dom intr) 'integerp)
      (in-tau-intervalp r intr)
      (tau-intervalp inti)
      (equal (tau-interval-dom inti) 'integerp)
      (in-tau-intervalp i inti))
    (and (tau-intervalp (tau-bounder-expt intr inti))
      (in-tau-intervalp (expt r i) (tau-bounder-expt intr inti))
      (implies (not (equal (tau-interval-dom (tau-bounder-expt intr inti))
            'integerp))
        (equal (tau-interval-dom (tau-bounder-expt intr inti))
          'rationalp))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-expt intr inti)))))

tau-bounder-ashfunction

(defun tau-bounder-ash
  (int1 int2)
  (declare (xargs :guard (and (tau-intervalp int1)
        (tau-intervalp int2)
        (equal (tau-interval-dom int1) 'integerp)
        (equal (tau-interval-dom int2) 'integerp))))
  (tau-bounder-floor (tau-bounder-* int1 (tau-bounder-expt2 int2))
    (make-tau-interval 'integerp nil 1 nil 1)))

tau-bounder-ash-correcttheorem

(defthm tau-bounder-ash-correct
  (implies (and (tau-intervalp int1)
      (tau-intervalp int2)
      (equal (tau-interval-dom int1) 'integerp)
      (equal (tau-interval-dom int2) 'integerp)
      (in-tau-intervalp x int1)
      (in-tau-intervalp y int2))
    (and (tau-intervalp (tau-bounder-ash int1 int2))
      (in-tau-intervalp (ash x y) (tau-bounder-ash int1 int2))
      (equal (tau-interval-dom (tau-bounder-ash int1 int2))
        'integerp)))
  :hints (("Goal" :use ((:instance tau-bounder-floor-correct
        (x (* x (expt 2 y)))
        (int1 (tau-bounder-* int1 (tau-bounder-expt2 int2)))
        (y 1)
        (int2 (make-tau-interval 'integerp nil 1 nil 1))))
     :in-theory (e/d (ash)
       (tau-intervalp in-tau-intervalp
         tau-bounder-floor
         tau-bounder-*
         tau-bounder-expt2
         tau-bounder-floor-correct
         (:executable-counterpart make-tau-interval)))))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tau-bounder-ash int1 int2)))))