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