		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass

Short-weierstrass->p

Get the p field from a short-weierstrass.

Signature
(short-weierstrass->p x) → p
Arguments: x — Guard (short-weierstrass-p x).
Returns: p — Type (natp p).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: short-weierstrass->p$inline

(defun short-weierstrass->p$inline (x)
  (declare (xargs :guard (short-weierstrass-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'short-weierstrass->p))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x))
              (p (nfix (cdr (std::da-nth 0 x))))
              (a (nfix (cdr (std::da-nth 1 x))))
              (b (nfix (cdr (std::da-nth 2 x)))))
           (if (and (> p 3)
                    (fep a p)
                    (fep b p)
                    (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))
               p
             5))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: natp-of-short-weierstrass->p

(defthm natp-of-short-weierstrass->p
  (b* ((p (short-weierstrass->p$inline x)))
    (natp p))
  :rule-classes :rewrite)

Theorem: short-weierstrass->p$inline-of-short-weierstrass-fix-x

(defthm short-weierstrass->p$inline-of-short-weierstrass-fix-x
  (equal (short-weierstrass->p$inline (short-weierstrass-fix x))
         (short-weierstrass->p$inline x)))

Theorem: short-weierstrass->p$inline-short-weierstrass-equiv-congruence-on-x

(defthm
 short-weierstrass->p$inline-short-weierstrass-equiv-congruence-on-x
 (implies (short-weierstrass-equiv x x-equiv)
          (equal (short-weierstrass->p$inline x)
                 (short-weierstrass->p$inline x-equiv)))
 :rule-classes :congruence)