		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-pgenstr-highest

(vl-pgenstr-highest prefix names) returns the largest n such that "prefix_n" occurs in names.

Signature
(vl-pgenstr-highest prefix names) → *
Arguments: prefix — Guard (stringp prefix).; names — Guard (string-listp names).

Definitions and Theorems

Function: vl-pgenstr-highest

(defun vl-pgenstr-highest (prefix names)
  (declare (xargs :guard (and (stringp prefix)
                              (string-listp names))))
  (let ((__function__ 'vl-pgenstr-highest))
    (declare (ignorable __function__))
    (cond ((atom names) 0)
          ((vl-pgenstr-p prefix (car names))
           (max (vl-pgenstr->val prefix (car names))
                (vl-pgenstr-highest prefix (cdr names))))
          (t (vl-pgenstr-highest prefix (cdr names))))))

Theorem: none-greater-than-vl-pgenstr-highest

(defthm none-greater-than-vl-pgenstr-highest
  (implies (and (< (vl-pgenstr-highest prefix names) n)
                (force (stringp prefix))
                (force (natp n)))
           (equal (member-equal (vl-pgenstr prefix n)
                                names)
                  nil)))

Theorem: vl-pgenstr-highest-of-incremental-extension

(defthm vl-pgenstr-highest-of-incremental-extension
 (implies
  (force (stringp prefix))
  (equal
     (vl-pgenstr-highest
          prefix
          (cons (vl-pgenstr prefix
                            (+ 1 (vl-pgenstr-highest prefix modns)))
                modns))
     (+ 1 (vl-pgenstr-highest prefix modns)))))

Theorem: vl-pgenstr-highest-of-irrelevant-extension

(defthm vl-pgenstr-highest-of-irrelevant-extension
 (implies
      (and (not (equal other prefix))
           (force (stringp prefix))
           (force (stringp other)))
      (equal (vl-pgenstr-highest other
                                 (cons (vl-pgenstr prefix k) modns))
             (vl-pgenstr-highest other modns))))