Optimized trailing 0 count for integers.
(trailing-1-count x) → *
To make this fast, be sure and include the "std/bitsets/bignum-extract-opt" book (reqires a ttag), which prevents this (at least on CCL64) from needing to create new bignums when run on bignums.
(defun trailing-1-count (x) (declare (xargs :guard (integerp x))) (let ((__function__ 'trailing-1-count)) (declare (ignorable __function__)) (mbe :logic (if (or (eql x -1) (not (logbitp 0 x))) 0 (+ 1 (trailing-1-count (logcdr x)))) :exec (if (eql -1 x) 0 (trailing-1-count-rec x 0)))))
(defthm trailing-1-count-is-trailing-0-count-of-lognot (equal (trailing-1-count x) (trailing-0-count (lognot x))))