Change names in
(vl-star-names-of-warning-wires x warning-wires) → new-x
Function:
(defun vl-star-names-of-warning-wires (x warning-wires) (declare (xargs :guard (and (string-listp x) (string-listp warning-wires)))) (let ((__function__ 'vl-star-names-of-warning-wires)) (declare (ignorable __function__)) (cond ((atom x) nil) ((member-equal (car x) warning-wires) (cons (cat (car x) "*") (vl-star-names-of-warning-wires (cdr x) warning-wires))) (t (cons (car x) (vl-star-names-of-warning-wires (cdr x) warning-wires))))))
Theorem:
(defthm string-listp-of-vl-star-names-of-warning-wires (implies (force (string-listp x)) (b* ((new-x (vl-star-names-of-warning-wires x warning-wires))) (string-listp new-x))) :rule-classes :rewrite)