		Search-engine friendly clone of the ACL2 documentation.

Logical-operations

Op-nand

Leo boolean negated conjunction operation.

Signature
(op-nand left right) → result
Arguments: left — Guard (valuep left).; right — Guard (valuep right).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-nand

(defun op-nand (left right)
  (declare (xargs :guard (and (valuep left) (valuep right))))
  (let ((__function__ 'op-nand))
    (declare (ignorable __function__))
    (if (and (value-case left :bool)
             (value-case right :bool))
        (value-bool (not (and (value-bool->get left)
                              (value-bool->get right))))
      (reserrf (list :op-nand (value-fix left)
                     (value-fix right))))))

Theorem: value-resultp-of-op-nand

(defthm value-resultp-of-op-nand
  (b* ((result (op-nand left right)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-nand-of-value-fix-left

(defthm op-nand-of-value-fix-left
  (equal (op-nand (value-fix left) right)
         (op-nand left right)))

Theorem: op-nand-value-equiv-congruence-on-left

(defthm op-nand-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-nand left right)
                  (op-nand left-equiv right)))
  :rule-classes :congruence)

Theorem: op-nand-of-value-fix-right

(defthm op-nand-of-value-fix-right
  (equal (op-nand left (value-fix right))
         (op-nand left right)))

Theorem: op-nand-value-equiv-congruence-on-right

(defthm op-nand-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-nand left right)
                  (op-nand left right-equiv)))
  :rule-classes :congruence)