		Search-engine friendly clone of the ACL2 documentation.

Boolean-if

Boolean-if-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-if-pred

(defun boolean-if-pred (x y z w prime)
  (and (equal (pfield::mul x (pfield::sub y z prime)
                           prime)
              (pfield::sub w z prime))))

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

(defthm definition-satp-to-boolean-if-pred
 (implies
  (and
   (equal
        (pfcs::lookup-definition '(:simple "boolean_if")
                                 pfcs::defs)
        '(:definition
              (name :simple "boolean_if")
              (pfcs::para (:simple "x")
                          (:simple "y")
                          (:simple "z")
                          (:simple "w"))
              (pfcs::body (:equal (:mul (:var (:simple "x"))
                                        (:sub (:var (:simple "y"))
                                              (:var (:simple "z"))))
                                  (:sub (:var (:simple "w"))
                                        (:var (:simple "z")))))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (pfield::fep z prime)
   (pfield::fep w prime)
   (primep prime))
  (equal (pfcs::definition-satp '(:simple "boolean_if")
                                pfcs::defs (list x y z w)
                                prime)
         (boolean-if-pred x y z w prime))))