		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-abs-s

Signature
(aabf-abs-s x man) → (mv xabs new-man)
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-abs-s

(defun aabf-abs-s (x man)
 (declare (xargs :guard (true-listp x)))
 (declare (xargs :guard (and (aabflist-p x man))))
 (let ((__function__ 'aabf-abs-s))
  (declare (ignorable __function__))
  (b* ((bound (aabf-integer-length-bound-s x man))
       (sign (aabf-sign-s x))
       (sign-lst (list sign)))
   (aabf-nest (aabf-loghead-ns
                   bound
                   (aabf-+-ss sign nil (aabf-logxor-ss sign-lst x)))
              man))))

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

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

Theorem: true-listp-of-aabf-abs-s.xabs

(defthm true-listp-of-aabf-abs-s.xabs
  (b* (((mv ?xabs ?new-man)
        (aabf-abs-s x man)))
    (true-listp xabs))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-abs-s

(defthm aabf-extension-p-of-aabf-abs-s
  (b* (((mv ?xabs ?new-man)
        (aabf-abs-s x man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-abs-s

(defthm aabf-p-of-aabf-abs-s
  (b* (((mv xabs new-man) (aabf-abs-s x man)))
    (implies (and (aabflist-p x man))
             (and (aabflist-p xabs new-man)))))

Theorem: aabf-eval-of-aabf-abs-s

(defthm aabf-eval-of-aabf-abs-s
 (b* (((mv xabs new-man) (aabf-abs-s x man)))
  (implies
       (and (aabflist-p x man))
       (and (equal (bools->int (aabflist-eval xabs env new-man))
                   (abs (bools->int (aabflist-eval x env man))))))))

Theorem: aabf-pred-of-aabf-abs-s

(defthm aabf-pred-of-aabf-abs-s
  (b* (((mv xabs new-man) (aabf-abs-s x man)))
    (implies (and (aabflist-p x man)
                  (aabflist-pred x man))
             (and (aabflist-pred xabs new-man)))))