Lift expdata-process-arg/res-list-surj to lists.
(expdata-process-arg/res-list-surj-list arg/res-list-surj-list k old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state) → (mv erp result state)
Function:
(defun expdata-process-arg/res-list-surj-list (arg/res-list-surj-list k old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (posp k) (symbolp old$) (booleanp verify-guards$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (symbol-listp names-to-avoid)))) (let ((__function__ 'expdata-process-arg/res-list-surj-list)) (declare (ignorable __function__)) (b* (((when (endp arg/res-list-surj-list)) (value (list arg-surjmaps res-surjmaps names-to-avoid))) ((er (list arg-surjmaps res-surjmaps names-to-avoid)) (expdata-process-arg/res-list-surj (car arg/res-list-surj-list) k old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state))) (expdata-process-arg/res-list-surj-list (cdr arg/res-list-surj-list) (1+ k) old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state))))