		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-abs-s

Signature
(bfr-abs-s x) → xabs
Arguments: x — Guard (true-listp x).
Returns: xabs — Type (true-listp xabs).

Definitions and Theorems

Function: bfr-abs-s

(defun bfr-abs-s (x)
 (declare (xargs :guard (true-listp x)))
 (let ((__function__ 'bfr-abs-s))
  (declare (ignorable __function__))
  (let ((sign (bfr-sign-s x)))
   (bfr-loghead-ns (integer-length-bound-s x)
                   (bfr-+-ss sign nil
                             (bfr-logxor-ss (bfr-sterm sign) x))))))

Theorem: true-listp-of-bfr-abs-s

(defthm true-listp-of-bfr-abs-s
  (b* ((xabs (bfr-abs-s x)))
    (true-listp xabs))
  :rule-classes :type-prescription)

Theorem: bfr-abs-s-correct

(defthm bfr-abs-s-correct
  (b* ((xabs (bfr-abs-s x)))
    (and (equal (bfr-list->s xabs env)
                (abs (bfr-list->s x env))))))

Theorem: bfr-abs-s-deps

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