Recognize elements of
(edwards-bls12-rstar-pointp x) → yes/no
These are the points of order
Function:
(defun edwards-bls12-rstar-pointp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'edwards-bls12-rstar-pointp)) (declare (ignorable acl2::__function__)) (and (edwards-bls12-pointp x) (twisted-edwards-point-orderp x (edwards-bls12-r) (edwards-bls12-curve)))))
Theorem:
(defthm booleanp-of-edwards-bls12-rstar-pointp (b* ((yes/no (edwards-bls12-rstar-pointp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm edwards-bls12-r-pointp-when-edwards-bls12-rstar-pointp (implies (edwards-bls12-rstar-pointp x) (edwards-bls12-r-pointp x)))