		Search-engine friendly clone of the ACL2 documentation.

Field-neq

Field-neq-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Theorem: field-neq-pred-suff

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

Theorem: definition-satp-to-field-neq-pred

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