		Search-engine friendly clone of the ACL2 documentation.

Boolean-not

Boolean-not-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-not-pred

(defun boolean-not-pred (x y prime)
  (and (equal (pfield::mul (pfield::sub (mod 1 prime) x prime)
                           (mod 1 prime)
                           prime)
              y)))

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

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