		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 "boolean_neq" pfcs::defs)
    '(:definition
       (pfcs::name . "boolean_neq")
       (pfcs::para "x" "y" "z")
       (pfcs::body (:relation "boolean_xor"
                              ((:var "x") (:var "y") (:var "z"))))))
   (equal
    (pfcs::lookup-definition "boolean_xor" pfcs::defs)
    '(:definition
        (pfcs::name . "boolean_xor")
        (pfcs::para "x" "y" "z")
        (pfcs::body (:equal (:mul (:mul (:const 2) (:var "x"))
                                  (:var "y"))
                            (:add (:add (:var "x") (:var "y"))
                                  (:mul (:const -1) (:var "z")))))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (pfield::fep z prime)
   (primep prime))
  (equal
       (pfcs::definition-satp "boolean_neq" pfcs::defs (list x y z)
                              prime)
       (boolean-neq-pred x y z prime))))