		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::sub (mod 1 prime) x prime)
                           (pfield::sub (mod 1 prime) y prime)
                           prime)
              (pfield::sub (mod 1 prime) z prime))))

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

(defthm definition-satp-to-boolean-or-pred
 (implies
  (and
   (equal
    (pfcs::lookup-definition '(:simple "boolean_or")
                             pfcs::defs)
    '(:definition
          (name :simple "boolean_or")
          (pfcs::para (:simple "x")
                      (:simple "y")
                      (:simple "z"))
          (pfcs::body
               (:equal (:mul (:sub (:const 1) (:var (:simple "x")))
                             (:sub (:const 1) (: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_or")
                                pfcs::defs (list x y z)
                                prime)
         (boolean-or-pred x y z prime))))