(update-parstate->tokens-unread tokens-unread parstate) → parstate
Function:
(defun update-parstate->tokens-unread (tokens-unread parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp tokens-unread))) (let ((__function__ 'update-parstate->tokens-unread)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->tokens-unread (nfix tokens-unread) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->tokens-unread (b* ((parstate (update-parstate->tokens-unread tokens-unread parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->tokens-unread-of-nfix-tokens-unread (equal (update-parstate->tokens-unread (nfix tokens-unread) parstate) (update-parstate->tokens-unread tokens-unread parstate)))
Theorem:
(defthm update-parstate->tokens-unread-nat-equiv-congruence-on-tokens-unread (implies (acl2::nat-equiv tokens-unread tokens-unread-equiv) (equal (update-parstate->tokens-unread tokens-unread parstate) (update-parstate->tokens-unread tokens-unread-equiv parstate))) :rule-classes :congruence)
Theorem:
(defthm update-parstate->tokens-unread-of-parstate-fix-parstate (equal (update-parstate->tokens-unread tokens-unread (parstate-fix parstate)) (update-parstate->tokens-unread tokens-unread parstate)))
Theorem:
(defthm update-parstate->tokens-unread-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (update-parstate->tokens-unread tokens-unread parstate) (update-parstate->tokens-unread tokens-unread parstate-equiv))) :rule-classes :congruence)