		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-logbitp-n2v

Signature
(sv::aig-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: aig-logbitp-n2v

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

Theorem: aig-logbitp-n2v-correct

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