		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-logbitp-n2v

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

Definitions and Theorems

Function: aabf-logbitp-n2v

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

Theorem: trivial-theorem-about-aabf-logbitp-n2v

(defthm trivial-theorem-about-aabf-logbitp-n2v
  (b* nil
    (b* ((?ignore (aabf-logbitp-n2v place digit n man)))
      t))
  :rule-classes nil)

Theorem: aabf-extension-p-of-aabf-logbitp-n2v

(defthm aabf-extension-p-of-aabf-logbitp-n2v
  (b* (((mv common-lisp::?bit ?new-man)
        (aabf-logbitp-n2v place digit n man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-logbitp-n2v

(defthm aabf-p-of-aabf-logbitp-n2v
  (b* (((mv bit new-man)
        (aabf-logbitp-n2v place digit n man)))
    (implies (and (aabflist-p digit man)
                  (aabflist-p n man))
             (and (aabf-p bit new-man)))))

Theorem: aabf-eval-of-aabf-logbitp-n2v

(defthm aabf-eval-of-aabf-logbitp-n2v
 (b* (((mv bit new-man)
       (aabf-logbitp-n2v place digit n man)))
  (implies
   (and (aabflist-p digit man)
        (aabflist-p n man))
   (and
     (equal (aabf-eval bit env new-man)
            (logbitp (* (pos-fix place)
                        (bools->uint (aabflist-eval digit env man)))
                     (bools->int (aabflist-eval n env man))))))))

Theorem: aabf-pred-of-aabf-logbitp-n2v

(defthm aabf-pred-of-aabf-logbitp-n2v
  (b* (((mv bit new-man)
        (aabf-logbitp-n2v place digit n man)))
    (implies (and (aabflist-p digit man)
                  (aabflist-p n man)
                  (aabflist-pred digit man)
                  (aabflist-pred n man))
             (and (aabf-pred bit new-man)))))