		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-car

Signature
(aabf-car vec) → bit
Arguments: vec — Guard (true-listp vec).

Definitions and Theorems

Function: aabf-car

(defun aabf-car (vec)
  (declare (xargs :guard (true-listp vec)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-car))
    (declare (ignorable __function__))
    (if (atom vec) (aabf-false) (car vec))))

Theorem: trivial-theorem-about-aabf-car

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

Theorem: aabf-p-of-aabf-car

(defthm aabf-p-of-aabf-car
  (b* ((bit (aabf-car vec)))
    (implies (and (aabflist-p vec man))
             (and (aabf-p bit man)))))

Theorem: aabf-eval-of-aabf-car

(defthm aabf-eval-of-aabf-car
 (b* ((bit (aabf-car vec)))
  (implies
   (and (aabflist-p vec man))
   (and
       (equal (aabf-eval bit env man)
              (intcar (bools->int (aabflist-eval vec env man))))))))

Theorem: aabf-pred-of-aabf-car

(defthm aabf-pred-of-aabf-car
  (b* ((bit (aabf-car vec)))
    (implies (and (aabflist-p vec man)
                  (aabflist-pred vec man))
             (and (aabf-pred bit man)))))