		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-all

Boolean-assert-all-circuit-body

Construct the defining body of the PFCS relation.

Signature
(boolean-assert-all-circuit-body xs) → constrs
Arguments: xs — Guard (name-listp xs).
Returns: constrs — Type (pfcs::constraint-listp constrs).

This is the list of boolean-assert calls, applied to each parameter. To facilitate proofs by induction, we define this construction over an arbitrary list of variable names, which are then instantiated to (x[0] ... x[n-1]).

Definitions and Theorems

Function: boolean-assert-all-circuit-body

(defun boolean-assert-all-circuit-body (xs)
  (declare (xargs :guard (name-listp xs)))
  (let ((__function__ 'boolean-assert-all-circuit-body))
    (declare (ignorable __function__))
    (cond ((endp xs) nil)
          (t (cons (pfcall (pfname "boolean_assert")
                           (pfvar (car xs)))
                   (boolean-assert-all-circuit-body (cdr xs)))))))

Theorem: constraint-listp-of-boolean-assert-all-circuit-body

(defthm constraint-listp-of-boolean-assert-all-circuit-body
  (b* ((constrs (boolean-assert-all-circuit-body xs)))
    (pfcs::constraint-listp constrs))
  :rule-classes :rewrite)

Theorem: sr1cs-constraint-listp-of-boolean-assert-all-circuit-body

(defthm sr1cs-constraint-listp-of-boolean-assert-all-circuit-body
  (b* ((constrs (boolean-assert-all-circuit-body xs)))
    (pfcs::sr1cs-constraint-listp constrs))
  :rule-classes :rewrite)

Theorem: constraint-list-vars-of-boolean-assert-all-circuit-body

(defthm constraint-list-vars-of-boolean-assert-all-circuit-body
 (equal
   (pfcs::constraint-list-vars (boolean-assert-all-circuit-body xs))
   (mergesort (name-list-fix xs))))