		Search-engine friendly clone of the ACL2 documentation.

Numbered-names-in-use

Max-numbered-name-index-in-use

Largest index of numbered name in use with a given base.

Signature
(max-numbered-name-index-in-use base wrld) → max-index
Arguments: base — Guard (symbolp base).; wrld — Guard (plist-worldp wrld).
Returns: max-index — Type (natp max-index).

Return the largest positive integer i such that the numbered name with base base and index i is in use (i.e. it is stored in the table). If no numbered name with base base is in use, return 0.

Definitions and Theorems

Function: max-numbered-name-index-in-use-aux

(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: natp-of-max-numbered-name-index-in-use-aux

(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: max-numbered-name-index-in-use

(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: natp-of-max-numbered-name-index-in-use

(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)