		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-equal-int-width

Signature
(sparseint$-equal-int-width width offset x y) → equal
Arguments: width — Guard (posp width).; offset — Guard (natp offset).; x — Guard (sparseint$-p x).; y — Guard (integerp y).
Returns: equal — Type (booleanp equal).

Definitions and Theorems

Function: sparseint$-equal-int-width

(defun sparseint$-equal-int-width (width offset x y)
 (declare (xargs :guard (and (posp width)
                             (natp offset)
                             (sparseint$-p x)
                             (integerp y))))
 (let ((__function__ 'sparseint$-equal-int-width))
  (declare (ignorable __function__))
  (b* ((width (lposfix width))
       (offset (lnfix offset))
       (y (lifix y)))
   (sparseint$-case
    x :leaf
    (equal (bignum-logext width (logtail offset x.val))
           y)
    :concat
    (b* (((when (<= x.width offset))
          (sparseint$-equal-int-width width (- offset x.width)
                                      x.msbs y))
         (width1 (- x.width offset))
         ((when (<= width width1))
          (sparseint$-equal-int-width width offset x.lsbs y)))
     (and
      (sparseint$-equal-int-width
           width1
           offset x.lsbs (bignum-logext width1 y))
      (sparseint$-equal-int-width (- width width1)
                                  0 x.msbs (logtail width1 y))))))))

Theorem: booleanp-of-sparseint$-equal-int-width

(defthm booleanp-of-sparseint$-equal-int-width
  (b* ((equal (sparseint$-equal-int-width width offset x y)))
    (booleanp equal))
  :rule-classes :type-prescription)

Theorem: sparseint$-equal-int-width-correct

(defthm sparseint$-equal-int-width-correct
  (b* ((common-lisp::?equal
            (sparseint$-equal-int-width width offset x y)))
    (equal equal
           (equal (logext width
                          (logtail offset (sparseint$-val x)))
                  (ifix y)))))

Theorem: sparseint$-equal-int-width-of-pos-fix-width

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

Theorem: sparseint$-equal-int-width-pos-equiv-congruence-on-width

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

Theorem: sparseint$-equal-int-width-of-nfix-offset

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

Theorem: sparseint$-equal-int-width-nat-equiv-congruence-on-offset

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

Theorem: sparseint$-equal-int-width-of-sparseint$-fix-x

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

Theorem: sparseint$-equal-int-width-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-equal-int-width-of-ifix-y

(defthm sparseint$-equal-int-width-of-ifix-y
  (equal (sparseint$-equal-int-width width offset x (ifix y))
         (sparseint$-equal-int-width width offset x y)))

Theorem: sparseint$-equal-int-width-int-equiv-congruence-on-y

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