• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
      • Index-permute-shrink
      • Permute-stretch
      • Env-mismatch-aux
      • Permute-shrink
      • Permute-polarity
      • Env-permute-polarity
      • Env-permute-shrink
      • Permute-var-down
      • Swap-vars-aux
      • Env-permute-stretch
      • Swap-vars
      • Permute-var-up
      • Negative-cofactor
      • Truth-perm-rev
      • Index-permute-stretch
      • Env-mismatch
      • Truth-perm
      • Swap-polarity
      • Positive-cofactor
      • Index-perm-rev
      • Env-perm-rev
      • Nth-set-bit-pos
      • Index-swap
      • Env-move-var-down
      • Is-xor-with-var
      • Index-perm
      • Env-swap-vars
      • Var
      • Truth-eval
      • Index-move-down
      • Env-update
      • Env-perm
      • Depends-on-witness
      • Env-swap-polarity
      • Var-repetitions
      • Env-move-var-up
      • Index-move-up
      • Depends-on
      • Truth-norm
      • Index-listp
      • Env-diff-index
      • Env-lookup
      • True
      • False
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Truth

Nth-set-bit-pos

Signature

(nth-set-bit-pos n x) → pos

Arguments

n — Guard (natp n).

x — Guard (integerp x).

Returns

pos — Type (or (natp pos) (not pos)).

Definitions and Theorems

Function: nth-set-bit-pos

(defun nth-set-bit-pos (n x)
       (declare (xargs :guard (and (natp n) (integerp x))))
       (let ((__function__ 'nth-set-bit-pos))
            (declare (ignorable __function__))
            (if (zip x)
                nil
                (b* ((bit (logcar x))
                     ((when (and (zp n) (eql bit 1))) 0)
                     (rest (nth-set-bit-pos (- (lnfix n) bit)
                                            (logcdr x))))
                    (and rest (+ 1 rest))))))

Theorem: return-type-of-nth-set-bit-pos

(defthm return-type-of-nth-set-bit-pos
        (b* ((pos (nth-set-bit-pos n x)))
            (or (natp pos) (not pos)))
        :rule-classes
        ((:type-prescription :typed-term (nth-set-bit-pos n x))))

Theorem: nth-set-bit-pos-of-negp

(defthm nth-set-bit-pos-of-negp
        (implies (negp x) (nth-set-bit-pos k x))
        :rule-classes (:rewrite :type-prescription))

Theorem: nth-set-bit-pos-exists-when-logcount

(defthm nth-set-bit-pos-exists-when-logcount
        (implies (< (nfix n) (logcount x))
                 (nth-set-bit-pos n x)))

Theorem: nth-set-bit-pos-types

(defthm nth-set-bit-pos-types
        (and (iff (acl2-numberp (nth-set-bit-pos n x))
                  (nth-set-bit-pos n x))
             (iff (rationalp (nth-set-bit-pos n x))
                  (nth-set-bit-pos n x))
             (iff (integerp (nth-set-bit-pos n x))
                  (nth-set-bit-pos n x))
             (iff (natp (nth-set-bit-pos n x))
                  (nth-set-bit-pos n x))))

Theorem: logcount-of-nth-set-bit-pos

(defthm logcount-of-nth-set-bit-pos
        (implies (nth-set-bit-pos k x)
                 (equal (logcount (loghead (nth-set-bit-pos k x) x))
                        (nfix k))))

Theorem: logbitp-of-nth-set-bit-pos

(defthm logbitp-of-nth-set-bit-pos
        (implies (nth-set-bit-pos n x)
                 (logbitp (nth-set-bit-pos n x) x)))

Theorem: logbitp-of-nth-set-bit-pos-lognot

(defthm logbitp-of-nth-set-bit-pos-lognot
        (implies (nth-set-bit-pos n (lognot x))
                 (not (logbitp (nth-set-bit-pos n (lognot x))
                               x))))

Theorem: nth-set-bit-pos-of-nfix-n

(defthm nth-set-bit-pos-of-nfix-n
        (equal (nth-set-bit-pos (nfix n) x)
               (nth-set-bit-pos n x)))

Theorem: nth-set-bit-pos-nat-equiv-congruence-on-n

(defthm nth-set-bit-pos-nat-equiv-congruence-on-n
        (implies (nat-equiv n n-equiv)
                 (equal (nth-set-bit-pos n x)
                        (nth-set-bit-pos n-equiv x)))
        :rule-classes :congruence)

Theorem: nth-set-bit-pos-of-ifix-x

(defthm nth-set-bit-pos-of-ifix-x
        (equal (nth-set-bit-pos n (ifix x))
               (nth-set-bit-pos n x)))

Theorem: nth-set-bit-pos-int-equiv-congruence-on-x

(defthm nth-set-bit-pos-int-equiv-congruence-on-x
        (implies (int-equiv x x-equiv)
                 (equal (nth-set-bit-pos n x)
                        (nth-set-bit-pos n x-equiv)))
        :rule-classes :congruence)

Theorem: index-permute-stretch-redef

(defthm
 index-permute-stretch-redef
 (equal
  (index-permute-stretch 0 count mask x numvars)
  (b*
     ((x (nfix x))
      (mask (nfix mask))
      (numvars (nfix numvars)))
     (cond ((< x (logcount (loghead numvars mask)))
            (nth-set-bit-pos x mask))
           ((< x numvars)
            (nth-set-bit-pos (- x (logcount (loghead numvars mask)))
                             (lognot mask)))
           (t x)))))