(sparseint$-trailing-0-count-width width offset negbit x) → count
Function:
(defun sparseint$-trailing-0-count-width (width offset negbit x) (declare (xargs :guard (and (posp width) (natp offset) (bitp negbit) (sparseint$-p x)))) (let ((__function__ 'sparseint$-trailing-0-count-width)) (declare (ignorable __function__)) (sparseint$-case x :leaf (b* (((when (mbe :logic (equal (logtail offset x.val) (- (lbfix negbit))) :exec (and (<= (integer-length x.val) (lnfix offset)) (eql negbit (logbit offset x.val))))) nil) (count (if (eql 1 negbit) (trailing-1-count-from x.val offset) (trailing-0-count-from x.val offset)))) (and (< count (lposfix width)) count)) :concat (b* ((width (lposfix width)) (offset (lnfix offset)) ((when (<= x.width offset)) (sparseint$-trailing-0-count-width width (- offset x.width) negbit x.msbs)) (width1 (- x.width offset)) ((when (<= width width1)) (sparseint$-trailing-0-count-width width offset negbit x.lsbs)) (lsb-count (sparseint$-trailing-0-count-width width1 offset negbit x.lsbs)) ((when lsb-count) lsb-count) (msb-count (sparseint$-trailing-0-count-width (- width width1) 0 negbit x.msbs))) (and msb-count (+ width1 msb-count))))))
Theorem:
(defthm maybe-natp-of-sparseint$-trailing-0-count-width (b* ((count (sparseint$-trailing-0-count-width width offset negbit x))) (acl2::maybe-natp count)) :rule-classes :type-prescription)
Theorem:
(defthm sparseint$-trailing-0-count-width-correct (b* ((common-lisp::?count (sparseint$-trailing-0-count-width width offset negbit x))) (and (iff count (not (equal (logext width (logtail offset (sparseint$-val x))) (- (bfix negbit))))) (implies (not (equal (logext width (logtail offset (sparseint$-val x))) (- (bfix negbit)))) (equal count (trailing-0-count (logxor (- (bfix negbit)) (logtail offset (sparseint$-val x)))))))))
Theorem:
(defthm sparseint$-trailing-0-count-width-of-pos-fix-width (equal (sparseint$-trailing-0-count-width (pos-fix width) offset negbit x) (sparseint$-trailing-0-count-width width offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-width-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-trailing-0-count-width width offset negbit x) (sparseint$-trailing-0-count-width width-equiv offset negbit x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-trailing-0-count-width-of-nfix-offset (equal (sparseint$-trailing-0-count-width width (nfix offset) negbit x) (sparseint$-trailing-0-count-width width offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-width-nat-equiv-congruence-on-offset (implies (nat-equiv offset offset-equiv) (equal (sparseint$-trailing-0-count-width width offset negbit x) (sparseint$-trailing-0-count-width width offset-equiv negbit x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-trailing-0-count-width-of-bfix-negbit (equal (sparseint$-trailing-0-count-width width offset (bfix negbit) x) (sparseint$-trailing-0-count-width width offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-width-bit-equiv-congruence-on-negbit (implies (bit-equiv negbit negbit-equiv) (equal (sparseint$-trailing-0-count-width width offset negbit x) (sparseint$-trailing-0-count-width width offset negbit-equiv x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-trailing-0-count-width-of-sparseint$-fix-x (equal (sparseint$-trailing-0-count-width width offset negbit (sparseint$-fix x)) (sparseint$-trailing-0-count-width width offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-width-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-trailing-0-count-width width offset negbit x) (sparseint$-trailing-0-count-width width offset negbit x-equiv))) :rule-classes :congruence)