		Search-engine friendly clone of the ACL2 documentation.

Bitops/extra-defs

Bitscan-fwd

(bitscan-fwd src) returns the bit position of the least significant bit in src that is set, or 0 when src is zero (and hence has no such bit).

Signature
(bitscan-fwd src) → position
Arguments: src — Guard (natp src).
Returns: position — Type (natp position).

Examples:

(bitscan-fwd #b1001) = 0
(bitscan-fwd #b1010) = 1
(bitscan-fwd #b1100) = 2
(bitscan-fwd #b1000) = 3

Definitions and Theorems

Function: bitscan-fwd

(defun bitscan-fwd (src)
  (declare (xargs :guard (natp src)))
  (let ((__function__ 'bitscan-fwd))
    (declare (ignorable __function__))
    (cond ((zp src) 0)
          ((logbitp 0 src) 0)
          (t (+ 1 (bitscan-fwd (ash src -1)))))))

Theorem: natp-of-bitscan-fwd

(defthm acl2::natp-of-bitscan-fwd
  (b* ((position (bitscan-fwd src)))
    (natp position))
  :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-bitscan-fwd-1

(defthm nat-equiv-implies-equal-bitscan-fwd-1
  (implies (nat-equiv src src-equiv)
           (equal (bitscan-fwd src)
                  (bitscan-fwd src-equiv)))
  :rule-classes (:congruence))