(sparseint$-trailing-0-count-rec offset negbit x) → count
Function:
(defun sparseint$-trailing-0-count-rec (offset negbit x) (declare (xargs :guard (and (natp offset) (bitp negbit) (sparseint$-p x)))) (let ((__function__ 'sparseint$-trailing-0-count-rec)) (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)) (if (eql negbit 1) (trailing-1-count-from x.val offset) (trailing-0-count-from x.val offset))) :concat (b* ((offset (lnfix offset)) ((when (<= x.width offset)) (sparseint$-trailing-0-count-rec (- offset x.width) negbit x.msbs)) (width1 (- x.width offset)) (lsbs-count (sparseint$-trailing-0-count-width width1 offset negbit x.lsbs)) ((when lsbs-count) lsbs-count) (msbs-count (sparseint$-trailing-0-count-rec 0 negbit x.msbs))) (and msbs-count (+ width1 msbs-count))))))
Theorem:
(defthm maybe-natp-of-sparseint$-trailing-0-count-rec (b* ((count (sparseint$-trailing-0-count-rec offset negbit x))) (acl2::maybe-natp count)) :rule-classes :type-prescription)
Theorem:
(defthm sparseint$-trailing-0-count-rec-correct (b* ((common-lisp::?count (sparseint$-trailing-0-count-rec offset negbit x))) (and (iff count (not (equal (logtail offset (sparseint$-val x)) (- (bfix negbit))))) (implies (not (equal (logtail offset (sparseint$-val x)) (- (bfix negbit)))) (equal count (trailing-0-count (logtail offset (logxor (- (bfix negbit)) (sparseint$-val x)))))))))
Theorem:
(defthm sparseint$-trailing-0-count-rec-of-nfix-offset (equal (sparseint$-trailing-0-count-rec (nfix offset) negbit x) (sparseint$-trailing-0-count-rec offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-rec-nat-equiv-congruence-on-offset (implies (nat-equiv offset offset-equiv) (equal (sparseint$-trailing-0-count-rec offset negbit x) (sparseint$-trailing-0-count-rec offset-equiv negbit x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-trailing-0-count-rec-of-bfix-negbit (equal (sparseint$-trailing-0-count-rec offset (bfix negbit) x) (sparseint$-trailing-0-count-rec offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-rec-bit-equiv-congruence-on-negbit (implies (bit-equiv negbit negbit-equiv) (equal (sparseint$-trailing-0-count-rec offset negbit x) (sparseint$-trailing-0-count-rec offset negbit-equiv x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-trailing-0-count-rec-of-sparseint$-fix-x (equal (sparseint$-trailing-0-count-rec offset negbit (sparseint$-fix x)) (sparseint$-trailing-0-count-rec offset negbit x)))
Theorem:
(defthm sparseint$-trailing-0-count-rec-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-trailing-0-count-rec offset negbit x) (sparseint$-trailing-0-count-rec offset negbit x-equiv))) :rule-classes :congruence)