Largest index of numbered name in use with a given base.
(max-numbered-name-index-in-use base wrld) → max-index
Return the largest positive integer
Function:
(defun max-numbered-name-index-in-use-aux (indices current-max-index) (declare (xargs :guard (and (pos-listp indices) (natp current-max-index)))) (let ((__function__ 'max-numbered-name-index-in-use-aux)) (declare (ignorable __function__)) (cond ((atom indices) (mbe :logic (nfix current-max-index) :exec current-max-index)) (t (max-numbered-name-index-in-use-aux (cdr indices) (max (car indices) current-max-index))))))
Theorem:
(defthm natp-of-max-numbered-name-index-in-use-aux (b* ((final-max-index (max-numbered-name-index-in-use-aux indices current-max-index))) (natp final-max-index)) :rule-classes :rewrite)
Function:
(defun max-numbered-name-index-in-use (base wrld) (declare (xargs :guard (and (symbolp base) (plist-worldp wrld)))) (let ((__function__ 'max-numbered-name-index-in-use)) (declare (ignorable __function__)) (let* ((tab (table-alist 'numbered-names-in-use wrld)) (current-indices (cdr (assoc-eq base tab)))) (max-numbered-name-index-in-use-aux current-indices 0))))
Theorem:
(defthm natp-of-max-numbered-name-index-in-use (b* ((max-index (max-numbered-name-index-in-use base wrld))) (natp max-index)) :rule-classes :rewrite)