### INTRODUCTORY-CHALLENGE-PROBLEM-3

challenge problem 3 for the new user of ACL2
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Start in a fresh ACL2, either by restarting your ACL2 image from scratch or
executing `:ubt! 1`

.

Define the following functions and use The Method to prove the theorem
at the bottom:

(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))
(defun dupsp (x) ; does x contain duplicate elements?
(if (endp x)
nil
(if (member (car x) (cdr x))
t
(dupsp (cdr x)))))

(defthm dupsp-rev
(equal (dupsp (rev x)) (dupsp x)))

When you've solved this problem, compare your answer to ours;
see introductory-challenge-problem-3-answer.

Then, use your browser's **Back Button** to return to
introductory-challenges.