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