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