		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-sign-s

Signature
(aabf-sign-s x) → sign
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-sign-s

(defun aabf-sign-s (x)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-sign-s))
    (declare (ignorable __function__))
    (b* (((mv first rest endp)
          (aabf-first/rest/end x))
         ((when endp) first))
      (aabf-sign-s rest))))

Theorem: trivial-theorem-about-aabf-sign-s

(defthm trivial-theorem-about-aabf-sign-s
  (b* nil
    (b* ((?ignore (aabf-sign-s x))) t))
  :rule-classes nil)

Theorem: aabf-p-of-aabf-sign-s

(defthm aabf-p-of-aabf-sign-s
  (b* ((sign (aabf-sign-s x)))
    (implies (and (aabflist-p x man))
             (and (aabf-p sign man)))))

Theorem: aabf-eval-of-aabf-sign-s

(defthm aabf-eval-of-aabf-sign-s
  (b* ((sign (aabf-sign-s x)))
    (implies (and (aabflist-p x man))
             (and (equal (aabf-eval sign env man)
                         (< (bools->int (aabflist-eval x env man))
                            0))))))

Theorem: aabf-pred-of-aabf-sign-s

(defthm aabf-pred-of-aabf-sign-s
  (b* ((sign (aabf-sign-s x)))
    (implies (and (aabflist-p x man)
                  (aabflist-pred x man))
             (and (aabf-pred sign man)))))