Logical exclusive disjunction
(boolean-xor operand-left operand-right) → result
Function:
(defun boolean-xor (operand-left operand-right) (declare (xargs :guard (and (boolean-valuep operand-left) (boolean-valuep operand-right)))) (b* ((x (boolean-value->bool operand-left)) (y (boolean-value->bool operand-right))) (boolean-value (not (equal x y)))))
Theorem:
(defthm boolean-valuep-of-boolean-xor (b* ((result (boolean-xor operand-left operand-right))) (boolean-valuep result)) :rule-classes :rewrite)
Theorem:
(defthm boolean-xor-commutative (equal (boolean-xor x y) (boolean-xor y x)))
Theorem:
(defthm boolean-xor-of-boolean-value-fix-operand-left (equal (boolean-xor (boolean-value-fix operand-left) operand-right) (boolean-xor operand-left operand-right)))
Theorem:
(defthm boolean-xor-boolean-value-equiv-congruence-on-operand-left (implies (boolean-value-equiv operand-left operand-left-equiv) (equal (boolean-xor operand-left operand-right) (boolean-xor operand-left-equiv operand-right))) :rule-classes :congruence)
Theorem:
(defthm boolean-xor-of-boolean-value-fix-operand-right (equal (boolean-xor operand-left (boolean-value-fix operand-right)) (boolean-xor operand-left operand-right)))
Theorem:
(defthm boolean-xor-boolean-value-equiv-congruence-on-operand-right (implies (boolean-value-equiv operand-right operand-right-equiv) (equal (boolean-xor operand-left operand-right) (boolean-xor operand-left operand-right-equiv))) :rule-classes :congruence)