		Search-engine friendly clone of the ACL2 documentation.

Points-fty

Point-finite

Build a finite elliptic curve point.

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

Definitions and Theorems

Function: point-finite

(defun point-finite (x y)
  (declare (xargs :guard (and (natp x) (natp y))))
  (let ((acl2::__function__ 'point-finite))
    (declare (ignorable acl2::__function__))
    (b* ((x (mbe :logic (nfix x) :exec x))
         (y (mbe :logic (nfix y) :exec y)))
      (cons x y))))

Theorem: pointp-of-point-finite

(defthm pointp-of-point-finite
  (b* ((p (point-finite x y))) (pointp p))
  :rule-classes :rewrite)

Theorem: point-kind-of-point-finite

(defthm point-kind-of-point-finite
  (equal (point-kind (point-finite x y))
         :finite))

Theorem: point-finite->x-of-point-finite

(defthm point-finite->x-of-point-finite
  (equal (point-finite->x (point-finite x y))
         (nfix x)))

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

(defthm point-finite->y-of-point-finite
  (equal (point-finite->y (point-finite x y))
         (nfix y)))

Theorem: point-finite-of-point-finite->x/y

(defthm point-finite-of-point-finite->x/y
  (implies (equal (point-kind p) :finite)
           (equal (point-finite (point-finite->x p)
                                (point-finite->y p))
                  (point-fix p))))

Theorem: point-fix-when-finite

(defthm point-fix-when-finite
  (implies (equal (point-kind p) :finite)
           (equal (point-fix p)
                  (point-finite (point-finite->x p)
                                (point-finite->y p)))))

Theorem: equal-of-point-finite

(defthm equal-of-point-finite
  (equal (equal (point-finite x y) p)
         (and (pointp p)
              (equal (point-kind p) :finite)
              (equal (point-finite->x p) (nfix x))
              (equal (point-finite->y p) (nfix y)))))

Theorem: point-finite-of-nfix-x

(defthm point-finite-of-nfix-x
  (equal (point-finite (nfix x) y)
         (point-finite x y)))

Theorem: point-finite-nat-equiv-congruence-on-x

(defthm point-finite-nat-equiv-congruence-on-x
  (implies (nat-equiv x x-equiv)
           (equal (point-finite x y)
                  (point-finite x-equiv y)))
  :rule-classes :congruence)

Theorem: point-finite-of-nfix-y

(defthm point-finite-of-nfix-y
  (equal (point-finite x (nfix y))
         (point-finite x y)))

Theorem: point-finite-nat-equiv-congruence-on-y

(defthm point-finite-nat-equiv-congruence-on-y
  (implies (nat-equiv y y-equiv)
           (equal (point-finite x y)
                  (point-finite x y-equiv)))
  :rule-classes :congruence)