		Search-engine friendly clone of the ACL2 documentation.

Boolean-xor

Boolean-xor-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-xor-pred

(defun boolean-xor-pred (x y z prime)
  (and (equal (pfield::mul (pfield::mul (mod 2 prime) x prime)
                           y prime)
              (pfield::sub (pfield::add x y prime)
                           z prime))))

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

(defthm definition-satp-to-boolean-xor-pred
 (implies
  (and
   (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"))
                                  (:sub (:add (:var "x") (:var "y"))
                                        (:var "z"))))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (pfield::fep z prime)
   (primep prime))
  (equal
       (pfcs::definition-satp "boolean_xor" pfcs::defs (list x y z)
                              prime)
       (boolean-xor-pred x y z prime))))