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