		Search-engine friendly clone of the ACL2 documentation.

Field-neq

Field-neq-correctness

Correctness of the circuit.

Soundness is proved by expanding predicate and specification, but we need to disable two distributive rules that interfere with the proof.

Completeness is proved by expanding the specification and then using the suff theorem for the predicate. The witness is 0 if x and y are equal, otherwise it is the quotient of z and x - y. We also need to disable a distributive rule that interferes.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-neq-pred-soundness

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

Theorem: field-neq-pred-completeness

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

Theorem: field-neq-pred-to-spec

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

Theorem: field-neq-circuit-to-spec

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