		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-bitcount-width

Signature
(sparseint$-bitcount-width width offset negbit x) → count
Arguments: width — Guard (posp width).; offset — Guard (natp offset).; negbit — Guard (bitp negbit).; x — Guard (sparseint$-p x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: sparseint$-bitcount-width

(defun sparseint$-bitcount-width (width offset negbit x)
 (declare (xargs :guard (and (posp width)
                             (natp offset)
                             (bitp negbit)
                             (sparseint$-p x))))
 (let ((__function__ 'sparseint$-bitcount-width))
  (declare (ignorable __function__))
  (sparseint$-case
   x :leaf
   (logcount
       (bignum-loghead (lposfix width)
                       (logtail offset
                                (logxor (- (lbfix negbit)) x.val))))
   :concat
   (b* ((width (lposfix width))
        (offset (lnfix offset))
        ((when (<= x.width offset))
         (sparseint$-bitcount-width width (- offset x.width)
                                    negbit x.msbs))
        (width1 (- x.width offset))
        ((when (<= width width1))
         (sparseint$-bitcount-width width offset negbit x.lsbs)))
     (+ (sparseint$-bitcount-width width1 offset negbit x.lsbs)
        (sparseint$-bitcount-width (- width width1)
                                   0 negbit x.msbs))))))

Theorem: natp-of-sparseint$-bitcount-width

(defthm natp-of-sparseint$-bitcount-width
  (b* ((count (sparseint$-bitcount-width width offset negbit x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: sparseint$-bitcount-width-correct

(defthm sparseint$-bitcount-width-correct
 (b* ((common-lisp::?count
           (sparseint$-bitcount-width width offset negbit x)))
  (equal
       count
       (logcount (loghead (pos-fix width)
                          (logtail offset
                                   (logxor (- (bfix negbit))
                                           (sparseint$-val x))))))))

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

(defthm sparseint$-bitcount-width-of-pos-fix-width
  (equal (sparseint$-bitcount-width (pos-fix width)
                                    offset negbit x)
         (sparseint$-bitcount-width width offset negbit x)))

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

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

Theorem: sparseint$-bitcount-width-of-nfix-offset

(defthm sparseint$-bitcount-width-of-nfix-offset
  (equal (sparseint$-bitcount-width width (nfix offset)
                                    negbit x)
         (sparseint$-bitcount-width width offset negbit x)))

Theorem: sparseint$-bitcount-width-nat-equiv-congruence-on-offset

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

Theorem: sparseint$-bitcount-width-of-bfix-negbit

(defthm sparseint$-bitcount-width-of-bfix-negbit
  (equal (sparseint$-bitcount-width width offset (bfix negbit)
                                    x)
         (sparseint$-bitcount-width width offset negbit x)))

Theorem: sparseint$-bitcount-width-bit-equiv-congruence-on-negbit

(defthm sparseint$-bitcount-width-bit-equiv-congruence-on-negbit
 (implies
    (bit-equiv negbit negbit-equiv)
    (equal (sparseint$-bitcount-width width offset negbit x)
           (sparseint$-bitcount-width width offset negbit-equiv x)))
 :rule-classes :congruence)

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

(defthm sparseint$-bitcount-width-of-sparseint$-fix-x
 (equal
  (sparseint$-bitcount-width width offset negbit (sparseint$-fix x))
  (sparseint$-bitcount-width width offset negbit x)))

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

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