		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-r-pointp

Recognize elements of r.

Signature
(edwards-bls12-r-pointp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

These are the points of order r.

Definitions and Theorems

Function: edwards-bls12-r-pointp

(defun edwards-bls12-r-pointp (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'edwards-bls12-r-pointp))
   (declare (ignorable acl2::__function__))
   (or (equal x (twisted-edwards-zero))
       (and (edwards-bls12-pointp x)
            (twisted-edwards-point-orderp x (edwards-bls12-r)
                                          (edwards-bls12-curve))))))

Theorem: booleanp-of-edwards-bls12-r-pointp

(defthm booleanp-of-edwards-bls12-r-pointp
  (b* ((yes/no (edwards-bls12-r-pointp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: edwards-bls12-pointp-when-edwards-bls12-r-pointp

(defthm edwards-bls12-pointp-when-edwards-bls12-r-pointp
  (implies (edwards-bls12-r-pointp x)
           (edwards-bls12-pointp x)))