Lifting of the circuit to a predicate.
Function:
(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:
(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))))