		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-pointp

Recognize elements of Edwards-BLS12 curve.

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

These are the points on the Edwards-BLS12 curve.

These are all finite points.

Definitions and Theorems

Function: edwards-bls12-pointp

(defun edwards-bls12-pointp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-pointp))
    (declare (ignorable acl2::__function__))
    (and (pointp x)
         (point-on-twisted-edwards-p x (edwards-bls12-curve)))))

Theorem: booleanp-of-edwards-bls12-pointp

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

Theorem: pointp-when-edwards-bls12-pointp

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

Theorem: point-finite-when-edwards-bls12-pointp

(defthm point-finite-when-edwards-bls12-pointp
  (implies (edwards-bls12-pointp x)
           (equal (point-kind x) :finite)))