		Search-engine friendly clone of the ACL2 documentation.

Field-div-unchecked

Field-div-unchecked-correctness

Correctness of the circuit.

The equivalence between predicate and specification is proved automatically via the prime fields library rules.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-div-unchecked-pred-to-spec

(defthm field-div-unchecked-pred-to-spec
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime)
                (not (equal y 0)))
           (equal (field-div-unchecked-pred x y z prime)
                  (field-div-unchecked-spec x y z prime))))

Theorem: field-div-unchecked-circuit-to-spec

(defthm field-div-unchecked-circuit-to-spec
 (implies
  (and
      (equal (pfcs::lookup-definition (pfname "field_div_unchecked")
                                      defs)
             (field-div-unchecked-circuit))
      (primep prime)
      (pfield::fep x prime)
      (pfield::fep y prime)
      (pfield::fep z prime)
      (not (equal y 0)))
  (equal (pfcs::definition-satp (pfname "field_div_unchecked")
                                defs (list x y z)
                                prime)
         (field-div-unchecked-spec x y z prime))))