Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Start in a fresh ACL2, either by restarting your ACL2 image from scratch or
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.