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