		Search-engine friendly clone of the ACL2 documentation.

Double-value-abs

Double-value-abs-fix

Fixer for double-value-abs.

Signature
(double-value-abs-fix x) → fixed-x
Arguments: x — Guard (double-value-abs-p x).
Returns: fixed-x — Type (double-value-abs-p fixed-x).

Definitions and Theorems

Function: double-value-abs-fix

(defun double-value-abs-fix (x)
  (declare (xargs :guard (double-value-abs-p x)))
  (mbe :logic
       (if (double-value-abs-p x)
           x
         (double-value-abs-pos-zero))
       :exec x))

Theorem: double-value-abs-p-of-double-value-abs-fix

(defthm double-value-abs-p-of-double-value-abs-fix
  (b* ((fixed-x (double-value-abs-fix x)))
    (double-value-abs-p fixed-x))
  :rule-classes :rewrite)

Theorem: double-value-abs-fix-when-double-value-abs-p

(defthm double-value-abs-fix-when-double-value-abs-p
  (implies (double-value-abs-p x)
           (equal (double-value-abs-fix x) x)))