Process an
(expdata-process-arg/res-list-surj arg/res-list-surj k old$ verify-guards$ arg-surjmaps res-surjmaps names-to-avoid ctx state) → (mv erp result state)
The
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)
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)
Function:
(defun expdata-process-arg/res-list-surj (arg/res-list-surj 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)) (declare (ignorable __function__)) (b* (((er &) (ensure-tuple$ arg/res-list-surj 2 (msg "The ~n0 component of the second input" (list k)) t nil)) (arg/res-list (first arg/res-list-surj)) (surj (second arg/res-list-surj)) ((er (list args ress)) (expdata-process-arg/res-list arg/res-list k old$ ctx state)) (arg-overlap (intersection-eq args (strip-cars arg-surjmaps))) ((when arg-overlap) (er-soft+ ctx t nil "The ~n0 component of the second input includes ~&1, ~ which are also present in the preceding components. ~ This violates the disjointness requirement." (list k) arg-overlap)) (res-overlap (intersection$ ress (strip-cars res-surjmaps))) ((when res-overlap) (er-soft+ ctx t nil "The ~n0 component of the second input includes ~ the ~s1 ~&2, ~ which ~s3 also present in the preceding components. ~ This violates the disjointness requirement." (list k) (if (= (len res-overlap) 1) "result with index" "results with indices") res-overlap (if (= (len res-overlap) 1) "is" "are"))) ((er (list surjmap names-to-avoid)) (expdata-process-surj surj k old$ verify-guards$ names-to-avoid ctx state)) (arg-surjmaps (expdata-process-arg/res-list-surj-add-args args surjmap arg-surjmaps)) (res-surjmaps (expdata-process-arg/res-list-surj-add-ress ress surjmap res-surjmaps))) (value (list arg-surjmaps res-surjmaps names-to-avoid)))))