(parstate->size parstate) → size
Function:
(defun parstate->size (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard t)) (let ((__function__ 'parstate->size)) (declare (ignorable __function__)) (mbe :logic (if (parstatep parstate) (raw-parstate->size parstate) 0) :exec (raw-parstate->size parstate))))
Theorem:
(defthm natp-of-parstate->size (b* ((size (parstate->size parstate))) (natp size)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm parstate->size-of-parstate-fix-parstate (equal (parstate->size (parstate-fix parstate)) (parstate->size parstate)))
Theorem:
(defthm parstate->size-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (parstate->size parstate) (parstate->size parstate-equiv))) :rule-classes :congruence)