		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::add x (pfield::mul (mod -1 prime) y prime)
                              prime)
                 w prime)
            z)
     (equal (pfield::mul
                 (pfield::add x (pfield::mul (mod -1 prime) y prime)
                              prime)
                 (pfield::add (mod 1 prime)
                              (pfield::mul (mod -1 prime) z prime)
                              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 (:add (:var "x")
                                     (:mul (:const -1) (:var "y")))
                               (:var "w"))
                         (:var "z"))
                 (:equal (:mul (:add (:var "x")
                                     (:mul (:const -1) (:var "y")))
                               (:add (:const 1)
                                     (:mul (: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))))