		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-all

Boolean-assert-all-correctness

Correctness of the circuit.

The equivalence between predicate and specification is proved by induction, via the equivalence theorem for single booleans and the specification predicates.

The extension to the circuit is boilerplate, given the lifting theorem.

Definitions and Theorems

Theorem: boolean-assert-all-pred-to-spec

(defthm boolean-assert-all-pred-to-spec
  (implies (and (primep prime)
                (pfield::fe-listp xs prime))
           (equal (boolean-assert-all-pred xs prime)
                  (bit-listp xs))))

Theorem: boolean-assert-all-circuit-to-spec

(defthm boolean-assert-all-circuit-to-spec
 (implies
  (and
   (equal
     (pfcs::lookup-definition (pfname "boolean_assert_all" (len xs))
                              defs)
     (boolean-assert-all-circuit (len xs)))
   (equal (pfcs::lookup-definition (pfname "boolean_assert")
                                   defs)
          (boolean-assert-circuit))
   (primep prime)
   (pfield::fe-listp xs prime))
  (equal
       (pfcs::definition-satp (pfname "boolean_assert_all" (len xs))
                              defs xs prime)
       (bit-listp xs))))