Walk down the partitioning alist and gather the names of all signals that Part might be a typo for.
(typo-find-plausible-typos1 part alist) → plausible-typos
Function:
(defun typo-find-plausible-typos1 (part alist) (declare (xargs :guard (and (character-list-listp part) (alistp alist)))) (declare (xargs :guard (and (vl-string-keys-p alist) (vl-character-list-list-values-p alist)))) (let ((__function__ 'typo-find-plausible-typos1)) (declare (ignorable __function__)) (cond ((atom alist) nil) ((typo-partitions-plausibly-typo-p part (cdar alist)) (cons (caar alist) (typo-find-plausible-typos1 part (cdr alist)))) (t (typo-find-plausible-typos1 part (cdr alist))))))
Theorem:
(defthm string-listp-of-typo-find-plausible-typos1 (implies (force (vl-string-keys-p alist)) (b* ((plausible-typos (typo-find-plausible-typos1 part alist))) (string-listp plausible-typos))) :rule-classes :rewrite)