		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-lognot-s

Signature
(bfr-lognot-s x) → nx
Arguments: x — Guard (true-listp x).
Returns: nx — Type (true-listp nx).

Definitions and Theorems

Function: bfr-lognot-s

(defun bfr-lognot-s (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'bfr-lognot-s))
    (declare (ignorable __function__))
    (b* (((mv head tail end) (first/rest/end x))
         ((when end) (bfr-sterm (bfr-not head))))
      (bfr-scons (bfr-not head)
                 (bfr-lognot-s tail)))))

Theorem: true-listp-of-bfr-lognot-s

(defthm true-listp-of-bfr-lognot-s
  (b* ((nx (bfr-lognot-s x)))
    (true-listp nx))
  :rule-classes :type-prescription)

Theorem: bfr-lognot-s-correct

(defthm bfr-lognot-s-correct
  (b* ((nx (bfr-lognot-s x)))
    (and (equal (bfr-list->s nx env)
                (lognot (bfr-list->s x env))))))

Theorem: bfr-lognot-s-deps

(defthm bfr-lognot-s-deps
  (b* ((nx (bfr-lognot-s x)))
    (implies (and (not (pbfr-list-depends-on varname param x)))
             (and (not (pbfr-list-depends-on varname param nx))))))