		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bittest-int-width

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

Definitions and Theorems

Function: sparseint$-binary-bittest-int-width

(defun sparseint$-binary-bittest-int-width (op width offset x y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (posp width)
                             (natp offset)
                             (sparseint$-p x)
                             (integerp y))))
 (let ((__function__ 'sparseint$-binary-bittest-int-width))
  (declare (ignorable __function__))
  (b*
    ((width (lposfix width))
     (offset (lnfix offset))
     (y (lifix y))
     ((when (or (eql y 0) (eql y -1)))
      (b* ((cofactor (binary-bitop-cofactor2 op (- y))))
        (sparseint$-unary-bittest-width cofactor width offset x))))
   (sparseint$-case
        x :leaf
        (binary-bittest op
                        (bignum-logext width (logtail offset x.val))
                        (bignum-logext width y))
        :concat
        (b* (((when (<= x.width offset))
              (sparseint$-binary-bittest-int-width
                   op width (- offset x.width)
                   x.msbs y))
             (width1 (- x.width offset))
             ((when (<= width width1))
              (sparseint$-binary-bittest-int-width
                   op width offset x.lsbs y)))
          (or (sparseint$-binary-bittest-int-width
                   op width1
                   offset x.lsbs (bignum-logext width1 y))
              (sparseint$-binary-bittest-int-width
                   op (- width width1)
                   0 x.msbs (logtail width1 y))))))))

Theorem: booleanp-of-sparseint$-binary-bittest-int-width

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

Theorem: sparseint$-val-of-sparseint$-binary-bittest-int-width

(defthm sparseint$-val-of-sparseint$-binary-bittest-int-width
  (b*
   ((?test
         (sparseint$-binary-bittest-int-width op width offset x y)))
   (equal
        test
        (binary-bittest op
                        (logext width
                                (logtail offset (sparseint$-val x)))
                        (logext width y)))))

Theorem: sparseint$-binary-bittest-int-width-of-ifix-op

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

Theorem: sparseint$-binary-bittest-int-width-int-equiv-congruence-on-op

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

Theorem: sparseint$-binary-bittest-int-width-of-pos-fix-width

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

Theorem: sparseint$-binary-bittest-int-width-pos-equiv-congruence-on-width

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

Theorem: sparseint$-binary-bittest-int-width-of-nfix-offset

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

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

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

Theorem: sparseint$-binary-bittest-int-width-of-sparseint$-fix-x

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

Theorem: sparseint$-binary-bittest-int-width-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-binary-bittest-int-width-of-ifix-y

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

Theorem: sparseint$-binary-bittest-int-width-int-equiv-congruence-on-y

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