		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-sign-s

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

Definitions and Theorems

Function: bfr-sign-s

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

Theorem: bfr-sign-s-correct

(defthm bfr-sign-s-correct
  (b* ((sign (bfr-sign-s x)))
    (and (equal (bfr-eval sign env)
                (< (bfr-list->s x env) 0)))))

Theorem: bfr-sign-s-deps

(defthm bfr-sign-s-deps
  (b* ((sign (bfr-sign-s x)))
    (implies (and (not (pbfr-list-depends-on varname param x)))
             (and (not (pbfr-depends-on varname param sign))))))