		Search-engine friendly clone of the ACL2 documentation.

Field-inv-flagged

Field-inv-flagged-correctness

Correctness of the circuit.

Soundness is proved automatically via the prime field library rules.

Completeness is proved via the suff theorem for the existentially quantified predicate. As witness for the internal variable w, we use the inverse of x if x \neq 0, otherwise we use 0 (but other values would work for this case).

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-inv-flagged-pred-soundness

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

Theorem: field-inv-flagged-pred-completeness

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

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

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

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

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