		Search-engine friendly clone of the ACL2 documentation.

Boolean-or

Boolean-or-circuit

Construction of the circuit.

Signature
(boolean-or-circuit) → pdef
Returns: pdef — Type (pfcs::definitionp pdef).

This is a PFCS definition with a single equality constraint of the form described in boolean-or.

An alternative definition could be in terms of the boolean-and and boolean-not circuits, but it is simpler to define this as a single equality constraint.

Definitions and Theorems

Function: boolean-or-circuit

(defun boolean-or-circuit nil
 (declare (xargs :guard t))
 (let ((__function__ 'boolean-or-circuit))
  (declare (ignorable __function__))
  (pfcs::parse-def
   "boolean_or(x, y, z) := {
    (1 + -1 * x) * (1 + -1 * y) == (1 + -1 * z)
    }")))

Theorem: definitionp-of-boolean-or-circuit

(defthm definitionp-of-boolean-or-circuit
  (b* ((pdef (boolean-or-circuit)))
    (pfcs::definitionp pdef))
  :rule-classes :rewrite)

Theorem: sr1cs-definitionp-of-boolean-or-circuit

(defthm sr1cs-definitionp-of-boolean-or-circuit
  (b* ((pdef (boolean-or-circuit)))
    (pfcs::sr1cs-definitionp pdef))
  :rule-classes :rewrite)