		Search-engine friendly clone of the ACL2 documentation.

Boolean-operations

Bool-not

Logical negation of boolean values.

Signature
(bool-not operand) → result
Arguments: operand — Guard (boolp operand).
Returns: result — Type (boolp result).

Definitions and Theorems

Function: bool-not

(defun bool-not (operand)
  (declare (xargs :guard (boolp operand)))
  (let ((__function__ 'bool-not))
    (declare (ignorable __function__))
    (b* ((x (bool->get operand)))
      (bool (not x)))))

Theorem: boolp-of-bool-not

(defthm boolp-of-bool-not
  (b* ((result (bool-not operand)))
    (boolp result))
  :rule-classes :rewrite)

Theorem: bool-not-of-bool-fix-operand

(defthm bool-not-of-bool-fix-operand
  (equal (bool-not (bool-fix operand))
         (bool-not operand)))

Theorem: bool-not-bool-equiv-congruence-on-operand

(defthm bool-not-bool-equiv-congruence-on-operand
  (implies (bool-equiv operand operand-equiv)
           (equal (bool-not operand)
                  (bool-not operand-equiv)))
  :rule-classes :congruence)