Get the time field from a svtv-probe.
(svtv-probe->time x) → time
This is an ordinary field accessor created by defprod.
Function:
(defun svtv-probe->time$inline (x) (declare (xargs :guard (svtv-probe-p x))) (declare (xargs :guard t)) (let ((__function__ 'svtv-probe->time)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (nfix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm natp-of-svtv-probe->time (b* ((time (svtv-probe->time$inline x))) (natp time)) :rule-classes :rewrite)
Theorem:
(defthm svtv-probe->time$inline-of-svtv-probe-fix-x (equal (svtv-probe->time$inline (svtv-probe-fix x)) (svtv-probe->time$inline x)))
Theorem:
(defthm svtv-probe->time$inline-svtv-probe-equiv-congruence-on-x (implies (svtv-probe-equiv x x-equiv) (equal (svtv-probe->time$inline x) (svtv-probe->time$inline x-equiv))) :rule-classes :congruence)