		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-ucons

Signature
(aabf-ucons b v) → res
Arguments: v — Guard (true-listp v).

Definitions and Theorems

Function: aabf-ucons

(defun aabf-ucons (b v)
  (declare (xargs :guard (true-listp v)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-ucons))
    (declare (ignorable __function__))
    (cons b (llist-fix v))))

Theorem: trivial-theorem-about-aabf-ucons

(defthm trivial-theorem-about-aabf-ucons
  (b* nil
    (b* ((?ignore (aabf-ucons b v))) t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-ucons.res

(defthm true-listp-of-aabf-ucons.res
  (b* ((?res (aabf-ucons b v)))
    (true-listp res))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-aabf-ucons

(defthm aabf-p-of-aabf-ucons
  (b* ((res (aabf-ucons b v)))
    (implies (and (aabf-p b man) (aabflist-p v man))
             (and (aabflist-p res man)))))

Theorem: aabf-eval-of-aabf-ucons

(defthm aabf-eval-of-aabf-ucons
 (b* ((res (aabf-ucons b v)))
  (implies
   (and (aabf-p b man) (aabflist-p v man))
   (and
       (equal (bools->uint (aabflist-eval res env man))
              (intcons (aabf-eval b env man)
                       (bools->uint (aabflist-eval v env man))))))))

Theorem: aabf-pred-of-aabf-ucons

(defthm aabf-pred-of-aabf-ucons
  (b* ((res (aabf-ucons b v)))
    (implies (and (aabf-p b man)
                  (aabflist-p v man)
                  (aabf-pred b man)
                  (aabflist-pred v man))
             (and (aabflist-pred res man)))))