		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-compare-offset

Signature
(sparseint$-compare-offset x y-offset y) → sign
Arguments: x — Guard (sparseint$-p x).; y-offset — Guard (natp y-offset).; y — Guard (sparseint$-p y).
Returns: sign — Type (integerp sign).

Definitions and Theorems

Function: sparseint$-compare-offset

(defun sparseint$-compare-offset (x y-offset y)
 (declare (xargs :guard (and (sparseint$-p x)
                             (natp y-offset)
                             (sparseint$-p y))))
 (let ((__function__ 'sparseint$-compare-offset))
  (declare (ignorable __function__))
  (b* ((y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
         y
         :leaf (compare x.val (logtail y-offset y.val))
         :concat (- (sparseint$-compare-int y-offset y x.val)))
    :concat
    (sparseint$-case
      y :leaf
      (sparseint$-compare-int 0 x (logtail y-offset y.val))
      :concat
      (b*
        (((when (<= y.width y-offset))
          (sparseint$-compare-offset x (- y-offset y.width)
                                     y.msbs))
         (msbs-compare
              (sparseint$-compare-offset x.msbs (+ x.width y-offset)
                                         y))
         ((unless (eql 0 msbs-compare))
          msbs-compare))
        (sparseint$-compare-width x.width x.lsbs y-offset y)))))))

Theorem: integerp-of-sparseint$-compare-offset

(defthm integerp-of-sparseint$-compare-offset
  (b* ((sign (sparseint$-compare-offset x y-offset y)))
    (integerp sign))
  :rule-classes :type-prescription)

Theorem: sparseint$-compare-offset-correct

(defthm sparseint$-compare-offset-correct
  (b* ((?sign (sparseint$-compare-offset x y-offset y)))
    (equal sign
           (compare (sparseint$-val x)
                    (logtail y-offset (sparseint$-val y))))))

Theorem: sparseint$-compare-offset-of-sparseint$-fix-x

(defthm sparseint$-compare-offset-of-sparseint$-fix-x
  (equal (sparseint$-compare-offset (sparseint$-fix x)
                                    y-offset y)
         (sparseint$-compare-offset x y-offset y)))

Theorem: sparseint$-compare-offset-sparseint$-equiv-congruence-on-x

(defthm sparseint$-compare-offset-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-compare-offset x y-offset y)
                  (sparseint$-compare-offset x-equiv y-offset y)))
  :rule-classes :congruence)

Theorem: sparseint$-compare-offset-of-nfix-y-offset

(defthm sparseint$-compare-offset-of-nfix-y-offset
  (equal (sparseint$-compare-offset x (nfix y-offset)
                                    y)
         (sparseint$-compare-offset x y-offset y)))

Theorem: sparseint$-compare-offset-nat-equiv-congruence-on-y-offset

(defthm sparseint$-compare-offset-nat-equiv-congruence-on-y-offset
  (implies (nat-equiv y-offset y-offset-equiv)
           (equal (sparseint$-compare-offset x y-offset y)
                  (sparseint$-compare-offset x y-offset-equiv y)))
  :rule-classes :congruence)

Theorem: sparseint$-compare-offset-of-sparseint$-fix-y

(defthm sparseint$-compare-offset-of-sparseint$-fix-y
  (equal (sparseint$-compare-offset x y-offset (sparseint$-fix y))
         (sparseint$-compare-offset x y-offset y)))

Theorem: sparseint$-compare-offset-sparseint$-equiv-congruence-on-y

(defthm sparseint$-compare-offset-sparseint$-equiv-congruence-on-y
  (implies (sparseint$-equiv y y-equiv)
           (equal (sparseint$-compare-offset x y-offset y)
                  (sparseint$-compare-offset x y-offset y-equiv)))
  :rule-classes :congruence)