Filter a sexpr-alist to avoid unnecessary onehot-rewriting.
Function:
(defun 4v-sexpr-mentions (x vars-fal) (declare (xargs :guard t)) (if (atom x) (hons-get x vars-fal) (4v-sexpr-list-mentions (cdr x) vars-fal)))
Function:
(defun 4v-sexpr-list-mentions (x vars-fal) (declare (xargs :guard t)) (if (atom x) nil (or (4v-sexpr-mentions (car x) vars-fal) (4v-sexpr-list-mentions (cdr x) vars-fal))))
Function:
(defun 4v-sexpr-mentions-memoize-condition (x vars-fal) (declare (ignorable x vars-fal) (xargs :guard 't)) (consp x))
Function:
(defun 4v-onehot-filter (x vars-fal keep skip) (declare (xargs :guard t)) (cond ((atom x) (mv keep skip)) ((atom (car x)) (4v-onehot-filter (cdr x) vars-fal keep skip)) ((4v-sexpr-mentions (cdar x) vars-fal) (4v-onehot-filter (cdr x) vars-fal (cons (car x) keep) skip)) (t (4v-onehot-filter (cdr x) vars-fal keep (cons (car x) skip)))))
Theorem:
(defthm 4v-onehot-filter-correct (b* (((mv keep skip) (4v-onehot-filter x vars-fal nil nil))) (implies (no-duplicatesp-equal (alist-keys x)) (equal (hons-assoc-equal key x) (or (hons-assoc-equal key keep) (hons-assoc-equal key skip))))) :rule-classes nil)