(update-parstate->char i char+pos parstate) → parstate
Function:
(defun update-parstate->char (i char+pos parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (natp i) (char+position-p char+pos)))) (declare (xargs :guard (< i (parstate->chars-length parstate)))) (let ((__function__ 'update-parstate->char)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (mbe :logic (if (< (nfix i) (parstate->chars-length parstate)) (raw-update-parstate->char (nfix i) (char+position-fix char+pos) parstate) parstate) :exec (raw-update-parstate->char i char+pos parstate)))))
Theorem:
(defthm parstatep-of-update-parstate->char (b* ((parstate (update-parstate->char i char+pos parstate))) (parstatep parstate)) :rule-classes :rewrite)