BOZO, terrible, inefficient.
(remove-each-from-alist keys alist) → *
Function:
(defun remove-each-from-alist (keys alist) (declare (xargs :guard (alistp alist))) (let ((__function__ 'remove-each-from-alist)) (declare (ignorable __function__)) (if (atom keys) alist (remove-each-from-alist (cdr keys) (remove-from-alist (car keys) alist)))))
Theorem:
(defthm vl-sigma-p-of-remove-from-alist (implies (vl-sigma-p alist) (vl-sigma-p (remove-from-alist key alist))))
Theorem:
(defthm vl-sigma-p-of-remove-each-from-alist (implies (vl-sigma-p alist) (vl-sigma-p (remove-each-from-alist keys alist))))
Theorem:
(defthm alistp-of-remove-each-from-alist (implies (alistp alist) (alistp (remove-each-from-alist keys alist))))