		Search-engine friendly clone of the ACL2 documentation.

Field-square

Field-square-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: field-square-pred

(defun field-square-pred (x y prime)
  (and (field-mul-pred x x y prime)))

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

(defthm definition-satp-to-field-square-pred
 (implies
  (and
   (equal
     (pfcs::lookup-definition '(:simple "field_square")
                              pfcs::defs)
     '(:definition (name :simple "field_square")
                   (pfcs::para (:simple "x") (:simple "y"))
                   (pfcs::body (:relation (:simple "field_mul")
                                          ((:var (:simple "x"))
                                           (:var (:simple "x"))
                                           (:var (:simple "y")))))))
   (equal
       (pfcs::lookup-definition '(:simple "field_mul")
                                pfcs::defs)
       '(:definition (name :simple "field_mul")
                     (pfcs::para (:simple "x")
                                 (:simple "y")
                                 (:simple "z"))
                     (pfcs::body (:equal (:mul (:var (:simple "x"))
                                               (:var (:simple "y")))
                                         (:var (:simple "z"))))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (primep prime))
  (equal (pfcs::definition-satp '(:simple "field_square")
                                pfcs::defs (list x y)
                                prime)
         (field-square-pred x y prime))))