		Search-engine friendly clone of the ACL2 documentation.

Vl-find-case-equivalent-strings

Vl-find-case-equivalent-strings-aux

Signature
(vl-find-case-equivalent-strings-aux x y) → equiv-sets
Arguments: x — Some subset of all the strings we're considering.
Guard (string-listp x).; y — The full list of all the strings, fixed.
Guard (string-listp y).
Returns: equiv-sets — Type (string-list-listp equiv-sets), given (string-listp y).

O(n^2) in the length of X, but X should be the list of duplicated strings, so there shouldn't be many.

Definitions and Theorems

Function: vl-find-case-equivalent-strings-aux

(defun vl-find-case-equivalent-strings-aux (x y)
  (declare (xargs :guard (and (string-listp x)
                              (string-listp y))))
  (let ((__function__ 'vl-find-case-equivalent-strings-aux))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (vl-collect-ieqv-strings (car x) y)
            (vl-find-case-equivalent-strings-aux (cdr x)
                                                 y)))))

Theorem: string-list-listp-of-vl-find-case-equivalent-strings-aux

(defthm string-list-listp-of-vl-find-case-equivalent-strings-aux
  (implies
       (string-listp y)
       (b* ((equiv-sets (vl-find-case-equivalent-strings-aux x y)))
         (string-list-listp equiv-sets)))
  :rule-classes :rewrite)