		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-equal-int

Signature
(sparseint$-equal-int offset x y) → equal
Arguments: 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

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

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

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

Theorem: sparseint$-equal-int-correct

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

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

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

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

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

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

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

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

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

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

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

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

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