		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-syntactically-zero-p

Signature
(aabf-syntactically-zero-p x) → result
Arguments: x — Guard (true-listp x).
Returns: result — Type (booleanp result).

Definitions and Theorems

Function: aabf-syntactically-zero-p

(defun aabf-syntactically-zero-p (x)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-syntactically-zero-p))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (aabf-syntactically-equal (car x)
                                     (aabf-false))
           (aabf-syntactically-zero-p (cdr x))))))

Theorem: booleanp-of-aabf-syntactically-zero-p

(defthm booleanp-of-aabf-syntactically-zero-p
  (b* ((result (aabf-syntactically-zero-p x)))
    (booleanp result))
  :rule-classes :rewrite)

Theorem: trivial-theorem-about-aabf-syntactically-zero-p

(defthm trivial-theorem-about-aabf-syntactically-zero-p
  (b* nil
    (b* ((?ignore (aabf-syntactically-zero-p x)))
      t))
  :rule-classes nil)

Theorem: aabf-syntactically-zero-p-implies

(defthm aabf-syntactically-zero-p-implies
  (b* nil
    (implies (aabf-syntactically-zero-p x)
             (equal (bools->int (aabflist-eval x env man))
                    0))))

Theorem: aabf-syntactically-zero-p-implies-unsigned

(defthm aabf-syntactically-zero-p-implies-unsigned
  (b* nil
    (implies (aabf-syntactically-zero-p x)
             (equal (bools->uint (aabflist-eval x env man))
                    0))))