		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-neg

Group point negation on Edwards-BLS12.

Signature
(edwards-bls12-neg point1) → point
Arguments: point1 — Guard (edwards-bls12-pointp point1).
Returns: point — Type (edwards-bls12-pointp point), given (edwards-bls12-pointp point1).

Definitions and Theorems

Function: edwards-bls12-neg

(defun edwards-bls12-neg (point1)
  (declare (xargs :guard (edwards-bls12-pointp point1)))
  (let ((acl2::__function__ 'edwards-bls12-neg))
    (declare (ignorable acl2::__function__))
    (twisted-edwards-neg point1 (edwards-bls12-curve))))

Theorem: edwards-bls12-pointp-of-edwards-bls12-neg

(defthm edwards-bls12-pointp-of-edwards-bls12-neg
  (implies (edwards-bls12-pointp point1)
           (b* ((point (edwards-bls12-neg point1)))
             (edwards-bls12-pointp point)))
  :rule-classes :rewrite)