		Search-engine friendly clone of the ACL2 documentation.

Casesplit-library-extensions

Negate-terms

Signature
(negate-terms terms) → negated-terms
Arguments: terms — Guard (pseudo-term-listp terms).
Returns: negated-terms — Type (pseudo-term-listp negated-terms), given (pseudo-term-listp terms).

Definitions and Theorems

Function: negate-terms

(defun negate-terms (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'negate-terms))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (cons (dumb-negate-lit (car terms))
                   (negate-terms (cdr terms)))))))

Theorem: pseudo-term-listp-of-negate-terms

(defthm pseudo-term-listp-of-negate-terms
  (implies (pseudo-term-listp terms)
           (b* ((negated-terms (negate-terms terms)))
             (pseudo-term-listp negated-terms)))
  :rule-classes :rewrite)