		Search-engine friendly clone of the ACL2 documentation.

Boolean-or

Boolean-or-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-or-pred

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

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

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