		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 "field_square" pfcs::defs)
    '(:definition
       (pfcs::name . "field_square")
       (pfcs::para "x" "y")
       (pfcs::body (:relation "field_mul"
                              ((:var "x") (:var "x") (:var "y"))))))
   (equal
      (pfcs::lookup-definition "field_mul" pfcs::defs)
      '(:definition (pfcs::name . "field_mul")
                    (pfcs::para "x" "y" "z")
                    (pfcs::body (:equal (:mul (:var "x") (:var "y"))
                                        (:var "z")))))
   (pfield::fep x prime)
   (pfield::fep y prime)
   (primep prime))
  (equal (pfcs::definition-satp "field_square" pfcs::defs (list x y)
                                prime)
         (field-square-pred x y prime))))