Concatenate the reverse of one list to another
The following theorem characterizes this English description.
(equal (revappend x y) (append (reverse x) y))
Hint: This lemma follows immediately from the definition of reverse and the following lemma.
(defthm revappend-append (equal (append (revappend x y) z) (revappend x (append y z))))
The guard for
(defun revappend (x y) (declare (xargs :guard (true-listp x))) (if (endp x) y (revappend (cdr x) (cons (car x) y))))