Tail-recursive implementation of append-alist-vals.
This is used in the implementation of
Theorem:
(defthm append-alist-vals-exec-removal (equal (append-alist-vals-exec x acc) (revappend (append-alist-vals x) acc)))
Function:
(defun append-alist-vals-exec (x acc) (declare (xargs :guard t)) (mbe :logic (if (atom x) acc (append-alist-vals-exec (cdr x) (revappend (cdar x) acc))) :exec (cond ((atom x) acc) ((atom (car x)) (append-alist-vals-exec (cdr x) acc)) (t (append-alist-vals-exec (cdr x) (revappend-without-guard (cdar x) acc))))))