		Search-engine friendly clone of the ACL2 documentation.

Boolean-neq

Boolean-neq-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-neq-pred

(defun boolean-neq-pred (x y z prime)
  (and (boolean-xor-pred x y z prime)))

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

(defthm definition-satp-to-boolean-neq-pred
 (implies
  (and
   (equal
     (pfcs::lookup-definition '(:simple "boolean_neq")
                              pfcs::defs)
     '(:definition (name :simple "boolean_neq")
                   (pfcs::para (:simple "x")
                               (:simple "y")
                               (:simple "z"))
                   (pfcs::body (:relation (:simple "boolean_xor")
                                          ((:var (:simple "x"))
                                           (:var (:simple "y"))
                                           (:var (:simple "z")))))))
   (equal
     (pfcs::lookup-definition '(:simple "boolean_xor")
                              pfcs::defs)
     '(:definition
           (name :simple "boolean_xor")
           (pfcs::para (:simple "x")
                       (:simple "y")
                       (:simple "z"))
           (pfcs::body
                (:equal (:mul (:mul (:const 2) (:var (:simple "x")))
                              (:var (:simple "y")))
                        (:sub (:add (:var (:simple "x"))
                                    (:var (:simple "y")))
                              (:var (:simple "z")))))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (pfield::fep z prime)
   (primep prime))
  (equal (pfcs::definition-satp '(:simple "boolean_neq")
                                pfcs::defs (list x y z)
                                prime)
         (boolean-neq-pred x y z prime))))