• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
      • Index-permute-shrink
      • Permute-stretch
      • Permute-shrink
      • Env-mismatch-aux
      • Env-permute-shrink
      • Permute-polarity
      • Env-permute-polarity
      • Permute-var-down
      • Env-permute-stretch
      • Swap-vars-aux
      • Swap-vars
      • Permute-var-up
      • Truth-perm-rev
      • Negative-cofactor
      • Index-permute-stretch
      • Env-mismatch
      • Swap-polarity
      • Positive-cofactor
      • Truth-perm
      • Index-perm-rev
      • Nth-set-bit-pos
      • Env-perm-rev
      • Is-xor-with-var
      • Index-swap
      • Index-perm
      • Env-move-var-down
      • Truth-eval
      • Env-swap-vars
      • Env-perm
      • Depends-on-witness
      • Var
      • Index-move-down
      • Env-update
      • Env-swap-polarity
      • Var-repetitions
      • Env-move-var-up
      • Depends-on
      • Index-move-up
      • 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
  • Math
  • Testing-utilities

• 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)))))