		Search-engine friendly clone of the ACL2 documentation.

Points-fty

Point-finite->y

Get the y coordinate of a finite elliptic curve point.

Signature
(point-finite->y p) → y
Arguments: p — Guard (pointp p).
Returns: y — Type (natp y).

Definitions and Theorems

Function: point-finite->y

(defun point-finite->y (p)
  (declare (xargs :guard (pointp p)))
  (declare (xargs :guard (equal (point-kind p) :finite)))
  (let ((acl2::__function__ 'point-finite->y))
    (declare (ignorable acl2::__function__))
    (b* ((p (mbe :logic (point-fix p) :exec p)))
      (if (consp p) (cdr p) 0))))

Theorem: natp-of-point-finite->y

(defthm natp-of-point-finite->y
  (b* ((y (point-finite->y p))) (natp y))
  :rule-classes :rewrite)

Theorem: point-finite->y-of-point-fix-p

(defthm point-finite->y-of-point-fix-p
  (equal (point-finite->y (point-fix p))
         (point-finite->y p)))

Theorem: point-finite->y-point-equiv-congruence-on-p

(defthm point-finite->y-point-equiv-congruence-on-p
  (implies (point-equiv p p-equiv)
           (equal (point-finite->y p)
                  (point-finite->y p-equiv)))
  :rule-classes :congruence)