(vl-collect-ieqv-strings-aux a x) → equiv-strs
Linear in the length of
Function:
(defun vl-collect-ieqv-strings-aux (a x) (declare (xargs :guard (and (stringp a) (string-listp x)))) (let ((__function__ 'vl-collect-ieqv-strings-aux)) (declare (ignorable __function__)) (cond ((atom x) nil) ((equal a (str::downcase-string (car x))) (cons (car x) (vl-collect-ieqv-strings-aux a (cdr x)))) (t (vl-collect-ieqv-strings-aux a (cdr x))))))
Theorem:
(defthm string-listp-of-vl-collect-ieqv-strings-aux (implies (string-listp x) (b* ((equiv-strs (vl-collect-ieqv-strings-aux a x))) (string-listp equiv-strs))) :rule-classes :rewrite)