		Search-engine friendly clone of the ACL2 documentation.

Boolean-operations

Bool-or

Logical disjunction of boolean values.

Signature
(bool-or left-operand right-operand) → result
Arguments: left-operand — Guard (boolp left-operand).; right-operand — Guard (boolp right-operand).
Returns: result — Type (boolp result).

Definitions and Theorems

Function: bool-or

(defun bool-or (left-operand right-operand)
  (declare (xargs :guard (and (boolp left-operand)
                              (boolp right-operand))))
  (let ((__function__ 'bool-or))
    (declare (ignorable __function__))
    (b* ((x (bool->get left-operand))
         (y (bool->get right-operand)))
      (bool (or x y)))))

Theorem: boolp-of-bool-or

(defthm boolp-of-bool-or
  (b* ((result (bool-or left-operand right-operand)))
    (boolp result))
  :rule-classes :rewrite)

Theorem: bool-or-of-bool-fix-left-operand

(defthm bool-or-of-bool-fix-left-operand
  (equal (bool-or (bool-fix left-operand)
                  right-operand)
         (bool-or left-operand right-operand)))

Theorem: bool-or-bool-equiv-congruence-on-left-operand

(defthm bool-or-bool-equiv-congruence-on-left-operand
  (implies (bool-equiv left-operand left-operand-equiv)
           (equal (bool-or left-operand right-operand)
                  (bool-or left-operand-equiv right-operand)))
  :rule-classes :congruence)

Theorem: bool-or-of-bool-fix-right-operand

(defthm bool-or-of-bool-fix-right-operand
  (equal (bool-or left-operand (bool-fix right-operand))
         (bool-or left-operand right-operand)))

Theorem: bool-or-bool-equiv-congruence-on-right-operand

(defthm bool-or-bool-equiv-congruence-on-right-operand
  (implies (bool-equiv right-operand right-operand-equiv)
           (equal (bool-or left-operand right-operand)
                  (bool-or left-operand right-operand-equiv)))
  :rule-classes :congruence)