		Search-engine friendly clone of the ACL2 documentation.

Field-div-flagged

Field-div-flagged-correctness

Correctness of the circuit.

Soundness is proved by expanding the predicate and specification, as well as pfield::div to expose pfield::inv, and we need a :use hint to apply a theorem in the right way.

Completeness is proved by expanding all the specifications, the correctness theorems for the called circuits, and using the suff theorem to obtain the conclusion. We also need to enable pfield::div; but here there is no need to disable the rule disabled in the soundness theorem (see above).

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-div-flagged-soundness

(defthm field-div-flagged-soundness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime)
                (pfield::fep e prime))
           (implies (field-div-flagged-pred x y z e prime)
                    (field-div-flagged-spec x y z e prime))))

Theorem: field-div-flagged-completeness

(defthm field-div-flagged-completeness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime)
                (pfield::fep e prime))
           (implies (field-div-flagged-spec x y z e prime)
                    (field-div-flagged-pred x y z e prime))))

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

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

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

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