		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass-curves

Short-weierstrass-primep

Check that the prime of a short Weierstrass curve is prime.

Signature
(short-weierstrass-primep curve) → yes/no
Arguments: curve — Guard (short-weierstrass-p curve).
Returns: yes/no — Type (booleanp yes/no).

This is in a separate predicate for the reason explained in short-weierstrass.

Definitions and Theorems

Function: short-weierstrass-primep

(defun short-weierstrass-primep (curve)
  (declare (xargs :guard (short-weierstrass-p curve)))
  (let ((acl2::__function__ 'short-weierstrass-primep))
    (declare (ignorable acl2::__function__))
    (dm::primep (short-weierstrass->p curve))))

Theorem: booleanp-of-short-weierstrass-primep

(defthm booleanp-of-short-weierstrass-primep
  (b* ((yes/no (short-weierstrass-primep curve)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: short-weierstrass-primep-of-short-weierstrass-fix-curve

(defthm short-weierstrass-primep-of-short-weierstrass-fix-curve
  (equal (short-weierstrass-primep (short-weierstrass-fix curve))
         (short-weierstrass-primep curve)))

Theorem: short-weierstrass-primep-short-weierstrass-equiv-congruence-on-curve

(defthm
 short-weierstrass-primep-short-weierstrass-equiv-congruence-on-curve
 (implies (short-weierstrass-equiv curve curve-equiv)
          (equal (short-weierstrass-primep curve)
                 (short-weierstrass-primep curve-equiv)))
 :rule-classes :congruence)