## REVAPPEND

concatentate the reverse of one list to another
Major Section: PROGRAMMING

`(Revappend x y)`

concatenates the reverse of the list `x`

to `y`

,
which is also typically a list.

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 `(revappend x y)`

requires that `x`

is a true list.

`Revappend`

is defined in Common Lisp. See any Common Lisp
documentation for more information.