|
|
|---|
|
|
|
|---|
Lifting of the circuit to a predicate.
Function:
(defun field-if-pred (x y z w prime) (and (equal (pfield::mul x (pfield::sub y z prime) prime) (pfield::sub w z 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") (:sub (:var "y") (:var "z"))) (:sub (:var "w") (: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))))