		Search-engine friendly clone of the ACL2 documentation.

Field-sub

Field-sub-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: field-sub-pred

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

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

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