Recognize elements of
(jubjub-pointp x) → yes/no
These are the points on the Jubjub curve.
These are all finite points.
(defun jubjub-pointp (x) (declare (xargs :guard t)) (let ((__function__ 'jubjub-pointp)) (declare (ignorable __function__)) (and (ecurve::pointp x) (point-on-jubjub-p x))))
(defthm booleanp-of-jubjub-pointp (b* ((yes/no (jubjub-pointp x))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm point-finite-when-jubjub-pointp (implies (jubjub-pointp x) (equal (ecurve::point-kind x) :finite)))