		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-compare-width

Signature
(sparseint$-compare-width width x y-offset y) → sign
Arguments: width — Guard (posp width).; 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-width

(defun sparseint$-compare-width (width x y-offset y)
 (declare (xargs :guard (and (posp width)
                             (sparseint$-p x)
                             (natp y-offset)
                             (sparseint$-p y))))
 (let ((__function__ 'sparseint$-compare-width))
  (declare (ignorable __function__))
  (b* ((width (lposfix width))
       (y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
        y :leaf
        (b* ((xval (bignum-loghead width x.val))
             (yval (bignum-loghead width (logtail y-offset y.val))))
          (compare xval yval))
        :concat (- (sparseint$-compare-int-width
                        width y-offset
                        y (bignum-loghead width x.val))))
    :concat
    (sparseint$-case
     y :leaf
     (sparseint$-compare-int-width
          width 0 x
          (bignum-loghead width (logtail y-offset y.val)))
     :concat
     (b* (((when (<= width x.width))
           (sparseint$-compare-width width x.lsbs y-offset y))
          ((when (<= y.width y-offset))
           (sparseint$-compare-width width x (- y-offset y.width)
                                     y.msbs))
          (y-width1 (- y.width y-offset))
          ((when (<= width y-width1))
           (sparseint$-compare-width width x y-offset y.lsbs))
          (msbs-compare
               (sparseint$-compare-width (- width x.width)
                                         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-width

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

Theorem: sparseint$-compare-width-correct

(defthm sparseint$-compare-width-correct
  (b* ((?sign (sparseint$-compare-width width x y-offset y)))
    (b* ((xval (loghead (pos-fix width)
                        (sparseint$-val x)))
         (yval (loghead (pos-fix width)
                        (logtail y-offset (sparseint$-val y)))))
      (equal sign (compare xval yval)))))

Theorem: sparseint$-compare-width-of-pos-fix-width

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

Theorem: sparseint$-compare-width-pos-equiv-congruence-on-width

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

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

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

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

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

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

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

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

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

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

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

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

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