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