		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-lognot-s

Signature
(aabf-lognot-s x man) → nx
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-lognot-s

(defun aabf-lognot-s (x man)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and (aabflist-p x man))))
  (let ((__function__ 'aabf-lognot-s))
    (declare (ignorable __function__))
    (b* (((mv head tail end)
          (aabf-first/rest/end x))
         ((when end) (list (aabf-not head man))))
      (aabf-scons (aabf-not head man)
                  (aabf-lognot-s tail man)))))

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

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

Theorem: true-listp-of-aabf-lognot-s.nx

(defthm true-listp-of-aabf-lognot-s.nx
  (b* ((?nx (aabf-lognot-s x man)))
    (true-listp nx))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-aabf-lognot-s

(defthm aabf-p-of-aabf-lognot-s
  (b* ((nx (aabf-lognot-s x man)))
    (implies (and (aabflist-p x man))
             (and (aabflist-p nx man)))))

Theorem: aabf-eval-of-aabf-lognot-s

(defthm aabf-eval-of-aabf-lognot-s
 (b* ((nx (aabf-lognot-s x man)))
  (implies
    (and (aabflist-p x man))
    (and (equal (bools->int (aabflist-eval nx env man))
                (lognot (bools->int (aabflist-eval x env man))))))))

Theorem: aabf-pred-of-aabf-lognot-s

(defthm aabf-pred-of-aabf-lognot-s
  (b* ((nx (aabf-lognot-s x man)))
    (implies (and (aabflist-p x man)
                  (aabflist-pred x man))
             (and (aabflist-pred nx man)))))