		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm

Svex-alistlist-removekeys

Signature
(svex-alistlist-removekeys keys alists) → *
Arguments: keys — Guard (svarlist-p keys).; alists — Guard (svex-alistlist-p alists).

Definitions and Theorems

Function: svex-alistlist-removekeys

(defun svex-alistlist-removekeys (keys alists)
  (declare (xargs :guard (and (svarlist-p keys)
                              (svex-alistlist-p alists))))
  (let ((__function__ 'svex-alistlist-removekeys))
    (declare (ignorable __function__))
    (if (atom alists)
        nil
      (cons (svex-alist-removekeys keys (car alists))
            (svex-alistlist-removekeys keys (cdr alists))))))

Theorem: svex-alistlist-removekeys-of-svarlist-fix-keys

(defthm svex-alistlist-removekeys-of-svarlist-fix-keys
  (equal (svex-alistlist-removekeys (svarlist-fix keys)
                                    alists)
         (svex-alistlist-removekeys keys alists)))

Theorem: svex-alistlist-removekeys-svarlist-equiv-congruence-on-keys

(defthm svex-alistlist-removekeys-svarlist-equiv-congruence-on-keys
  (implies (svarlist-equiv keys keys-equiv)
           (equal (svex-alistlist-removekeys keys alists)
                  (svex-alistlist-removekeys keys-equiv alists)))
  :rule-classes :congruence)

Theorem: svex-alistlist-removekeys-of-svex-alistlist-fix-alists

(defthm svex-alistlist-removekeys-of-svex-alistlist-fix-alists
 (equal (svex-alistlist-removekeys keys (svex-alistlist-fix alists))
        (svex-alistlist-removekeys keys alists)))

Theorem: svex-alistlist-removekeys-svex-alistlist-equiv-congruence-on-alists

(defthm
 svex-alistlist-removekeys-svex-alistlist-equiv-congruence-on-alists
 (implies (svex-alistlist-equiv alists alists-equiv)
          (equal (svex-alistlist-removekeys keys alists)
                 (svex-alistlist-removekeys keys alists-equiv)))
 :rule-classes :congruence)