		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert

Boolean-assert-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-assert-pred

(defun boolean-assert-pred (x prime)
 (and
  (equal
      (pfield::mul (pfield::add (mod 1 prime)
                                (pfield::mul (mod -1 prime) x prime)
                                prime)
                   x prime)
      (mod 0 prime))))

Theorem: definition-satp-to-boolean-assert-pred

(defthm definition-satp-to-boolean-assert-pred
 (implies
  (and
   (equal
    (pfcs::lookup-definition "boolean_assert" pfcs::defs)
    '(:definition
      (pfcs::name . "boolean_assert")
      (pfcs::para "x")
      (pfcs::body (:equal (:mul (:add (:const 1)
                                      (:mul (:const -1) (:var "x")))
                                (:var "x"))
                          (:const 0)))))
   (pfield::fep x prime)
   (primep prime))
  (equal (pfcs::definition-satp "boolean_assert" pfcs::defs (list x)
                                prime)
         (boolean-assert-pred x prime))))