		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-all

Boolean-assert-all-circuit

Construction of the circuit.

Signature
(boolean-assert-all-circuit n) → pdef
Arguments: n — Guard (natp n).
Returns: pdef — Type (pfcs::definitionp pdef).

The construction is parameterized by n.

The name of the circuit includes the parameter n, so that a larger circuit can include different instances of this circuit without conflict.

The parameter list is (x_0 ... x[n-1>).

Definitions and Theorems

Function: boolean-assert-all-circuit

(defun boolean-assert-all-circuit (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'boolean-assert-all-circuit))
    (declare (ignorable __function__))
    (b* ((para (pfnames "x" n)))
      (pfdef (pfname "boolean_assert_all" n)
             para
             (boolean-assert-all-circuit-body para)))))

Theorem: definitionp-of-boolean-assert-all-circuit

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

Theorem: sr1cs-definitionp-of-boolean-assert-all-circuit

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

Theorem: definition->name-of-boolean-assert-all-circuit

(defthm definition->name-of-boolean-assert-all-circuit
  (equal (pfcs::definition->name (boolean-assert-all-circuit n))
         (pfname "boolean_assert_all" n)))

Theorem: definition->para-of-boolean-assert-all-circuit

(defthm definition->para-of-boolean-assert-all-circuit
  (equal (pfcs::definition->para (boolean-assert-all-circuit n))
         (pfnames "x" n)))

Theorem: definition->body-of-boolean-assert-all-circuit

(defthm definition->body-of-boolean-assert-all-circuit
  (equal (pfcs::definition->body (boolean-assert-all-circuit n))
         (boolean-assert-all-circuit-body (pfnames "x" n))))

Theorem: definition-free-vars-of-boolean-assert-all-circuit

(defthm definition-free-vars-of-boolean-assert-all-circuit
  (emptyp
       (pfcs::definition-free-vars (boolean-assert-all-circuit n))))