		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-scons

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

Definitions and Theorems

Function: aabf-scons

(defun aabf-scons (b v)
  (declare (xargs :guard (true-listp v)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-scons))
    (declare (ignorable __function__))
    (b* ((v (llist-fix v)))
      (if (atom v)
          (if (aabf-syntactically-equal b (aabf-false))
              (list (aabf-false))
            (list b (aabf-false)))
        (if (s-endp v)
            (if (aabf-syntactically-equal b (car v))
                v
              (cons b v))
          (cons b v))))))

Theorem: trivial-theorem-about-aabf-scons

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

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

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

Theorem: aabf-p-of-aabf-scons

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

Theorem: aabf-eval-of-aabf-scons

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

Theorem: aabf-pred-of-aabf-scons

(defthm aabf-pred-of-aabf-scons
  (b* ((res (aabf-scons 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)))))