		Search-engine friendly clone of the ACL2 documentation.

Field-div-flagged

Field-div-flagged-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Theorem: field-div-flagged-pred-suff

(defthm field-div-flagged-pred-suff
  (implies (and (pfield::fep w prime)
                (and (equal (pfield::mul y w prime)
                            (pfield::sub (mod 1 prime) e prime))
                     (equal (pfield::mul y e prime)
                            (mod 0 prime))
                     (equal (pfield::mul x w prime) z)
                     (equal (pfield::mul z e prime)
                            (mod 0 prime))))
           (field-div-flagged-pred x y z e prime)))

Theorem: definition-satp-to-field-div-flagged-pred

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