		Search-engine friendly clone of the ACL2 documentation.

Boolean-nand

Boolean-nand-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-nand-pred

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

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

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