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