(4v-alist->faig-const-alist x) → *
Function:
(defun 4v-alist->faig-const-alist (x) (declare (xargs :guard t)) (let ((__function__ '4v-alist->faig-const-alist)) (declare (ignorable __function__)) (cond ((atom x) nil) ((atom (car x)) (4v-alist->faig-const-alist (cdr x))) (t (cons (cons (caar x) (4v->faig-const (cdar x))) (4v-alist->faig-const-alist (cdr x)))))))
Theorem:
(defthm hons-assoc-equal-4v-alist->faig-const-alist (equal (hons-assoc-equal k (4v-alist->faig-const-alist al)) (and (hons-assoc-equal k al) (cons k (4v->faig-const (cdr (hons-assoc-equal k al)))))))