INTRODUCTORY-CHALLENGE-PROBLEM-3

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.