Get the
Function:
(defun point-finite->x (p) (declare (xargs :guard (pointp p))) (declare (xargs :guard (equal (point-kind p) :finite))) (let ((acl2::__function__ 'point-finite->x)) (declare (ignorable acl2::__function__)) (b* ((p (mbe :logic (point-fix p) :exec p))) (if (consp p) (car p) 0))))
Theorem:
(defthm natp-of-point-finite->x (b* ((x (point-finite->x p))) (natp x)) :rule-classes :rewrite)
Theorem:
(defthm point-finite->x-of-point-fix-p (equal (point-finite->x (point-fix p)) (point-finite->x p)))
Theorem:
(defthm point-finite->x-point-equiv-congruence-on-p (implies (point-equiv p p-equiv) (equal (point-finite->x p) (point-finite->x p-equiv))) :rule-classes :congruence)