		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-logbitp-n2v

Signature
(bfr-logbitp-n2v place digit n) → bit
Arguments: place — Guard (posp place).; digit — Guard (true-listp digit).; n — Guard (true-listp n).

Definitions and Theorems

Function: bfr-logbitp-n2v

(defun bfr-logbitp-n2v (place digit n)
  (declare (xargs :guard (and (posp place)
                              (true-listp digit)
                              (true-listp n))))
  (let ((__function__ 'bfr-logbitp-n2v))
    (declare (ignorable __function__))
    (b* (((mv first & end) (first/rest/end n))
         (place (lposfix place))
         ((when (or (atom digit) end)) first))
      (bfr-ite (car digit)
               (bfr-logbitp-n2v (* 2 place)
                                (cdr digit)
                                (bfr-logtail-ns place n))
               (bfr-logbitp-n2v (* 2 place)
                                (cdr digit)
                                n)))))

Theorem: bfr-logbitp-n2v-correct

(defthm bfr-logbitp-n2v-correct
  (b* ((bit (bfr-logbitp-n2v place digit n)))
    (and (equal (bfr-eval bit env)
                (logbitp (* (pos-fix place)
                            (bfr-list->u digit env))
                         (bfr-list->s n env))))))

Theorem: bfr-logbitp-n2v-deps

(defthm bfr-logbitp-n2v-deps
  (b* ((bit (bfr-logbitp-n2v place digit n)))
    (implies (and (not (pbfr-list-depends-on varname param digit))
                  (not (pbfr-list-depends-on varname param n)))
             (and (not (pbfr-depends-on varname param bit))))))