		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-sign-abs-not-s

Signature
(aabf-sign-abs-not-s x man) → (mv s a n new-man)
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-sign-abs-not-s

(defun aabf-sign-abs-not-s (x man)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and (aabflist-p x man))))
  (let ((__function__ 'aabf-sign-abs-not-s))
    (declare (ignorable __function__))
    (b* (((mv abs man) (aabf-abs-s x man)))
      (mv (aabf-sign-s x)
          abs (aabf-lognot-s abs man)
          man))))

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

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

Theorem: true-listp-of-aabf-sign-abs-not-s.a

(defthm true-listp-of-aabf-sign-abs-not-s.a
  (b* (((mv acl2::?s acl2::?a acl2::?n ?new-man)
        (aabf-sign-abs-not-s x man)))
    (true-listp a))
  :rule-classes :type-prescription)

Theorem: true-listp-of-aabf-sign-abs-not-s.n

(defthm true-listp-of-aabf-sign-abs-not-s.n
  (b* (((mv acl2::?s acl2::?a acl2::?n ?new-man)
        (aabf-sign-abs-not-s x man)))
    (true-listp n))
  :rule-classes :type-prescription)

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

(defthm aabf-extension-p-of-aabf-sign-abs-not-s
  (b* (((mv acl2::?s acl2::?a acl2::?n ?new-man)
        (aabf-sign-abs-not-s x man)))
    (aabf-extension-p new-man man)))

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

(defthm aabf-p-of-aabf-sign-abs-not-s
  (b* (((mv s a n new-man)
        (aabf-sign-abs-not-s x man)))
    (implies (and (aabflist-p x man))
             (and (aabf-p s new-man)
                  (aabflist-p a new-man)
                  (aabflist-p n new-man)))))

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

(defthm aabf-eval-of-aabf-sign-abs-not-s
 (b* (((mv s a n new-man)
       (aabf-sign-abs-not-s x man)))
  (implies
   (and (aabflist-p x man))
   (and
     (equal (aabf-eval s env new-man)
            (< (bools->int (aabflist-eval x env man))
               0))
     (equal (bools->int (aabflist-eval a env new-man))
            (abs (bools->int (aabflist-eval x env man))))
     (equal
          (bools->int (aabflist-eval n env new-man))
          (lognot (abs (bools->int (aabflist-eval x env man)))))))))

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

(defthm aabf-pred-of-aabf-sign-abs-not-s
  (b* (((mv s a n new-man)
        (aabf-sign-abs-not-s x man)))
    (implies (and (aabflist-p x man)
                  (aabflist-pred x man))
             (and (aabf-pred s new-man)
                  (aabflist-pred a new-man)
                  (aabflist-pred n new-man)))))