		Search-engine friendly clone of the ACL2 documentation.

Field-if

Field-if-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: field-if-pred

(defun field-if-pred (x y z w prime)
 (and
  (equal
    (pfield::mul x
                 (pfield::add y (pfield::mul (mod -1 prime) z prime)
                              prime)
                 prime)
    (pfield::add w (pfield::mul (mod -1 prime) z prime)
                 prime))))

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

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