(vl-find-case-equivalent-strings-aux x y) → equiv-sets
O(n^2) in the length of X, but X should be the list of duplicated strings, so there shouldn't be many.
Function:
(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:
(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)