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