(expdata-process-arg/res-list-surj-add-ress ress surjmap res-surjmaps) → new-res-surjmaps
Function:
(defun expdata-process-arg/res-list-surj-add-ress (ress surjmap res-surjmaps) (declare (xargs :guard (and (pos-listp ress) (expdata-surjmapp surjmap) (expdata-pos-surjmap-alistp res-surjmaps)))) (let ((__function__ 'expdata-process-arg/res-list-surj-add-ress)) (declare (ignorable __function__)) (cond ((endp ress) res-surjmaps) (t (expdata-process-arg/res-list-surj-add-ress (cdr ress) surjmap (acons (car ress) surjmap res-surjmaps))))))
Theorem:
(defthm expdata-pos-surjmap-alistp-of-expdata-process-arg/res-list-surj-add-ress (implies (and (pos-listp ress) (expdata-surjmapp surjmap) (expdata-pos-surjmap-alistp res-surjmaps)) (b* ((new-res-surjmaps (expdata-process-arg/res-list-surj-add-ress ress surjmap res-surjmaps))) (expdata-pos-surjmap-alistp new-res-surjmaps))) :rule-classes :rewrite)