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

This answer is in the form of a script sufficient to lead ACL2 to a proof.

```; Trying `dupsp-rev` at this point produces the key checkpoint:

; (IMPLIES (AND (CONSP X)
;               (NOT (MEMBER (CAR X) (CDR X)))
;               (EQUAL (DUPSP (REV (CDR X)))
;                      (DUPSP (CDR X))))
;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
;                 (DUPSP (CDR X))))

; which suggests the lemma

; (defthm dupsp-append
;   (implies (not (member e x))
;            (equal (dupsp (append x (list e)))
;                   (dupsp x))))

; However, attempting to prove that, produces a key checkpoint
; containing `(MEMBER (CAR X) (APPEND (CDR X) (LIST E)))`.
; So we prove the lemma:

(defthm member-append
(iff (member e (append a b))
(or (member e a)
(member e b))))

; Note that we had to use `iff` instead of `equal` since `member` is not a
; Boolean function.

; Having proved this lemma, we return to `dupsp-append` and succeed:

(defthm dupsp-append
(implies (not (member e x))
(equal (dupsp (append x (list e)))
(dupsp x))))

; So now we return to `dups-rev`, expecting success.  But it fails
; with the same key checkpoint:

; (IMPLIES (AND (CONSP X)
;               (NOT (MEMBER (CAR X) (CDR X)))
;               (EQUAL (DUPSP (REV (CDR X)))
;                      (DUPSP (CDR X))))
;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
;                 (DUPSP (CDR X))))

; Why wasn't our `dupsp-append` lemma applied?  We have two choices here:
; (1) Think.  (2) Use tools.

; Think:  When an enabled rewrite rule doesn't fire even though the left-hand
; side matches the target, the hypothesis couldn't be relieved.  The `dups-append`
; rule has the hypothesis `(not (member e x))` and after the match with the left-hand side,
; `e` is `(CAR X)` and `x` is `(REV (CDR X))`.  So the system couldn't rewrite
; `(NOT (MEMBER (CAR X) (REV (CDR X))))` to true, even though it knows that
; `(NOT (MEMBER (CAR X) (CDR X)))` from the second hypothesis of the checkpoint.
; Obviously, we need to prove `member-rev` below.

; Use tools:  We could enable the ``break rewrite'' facility, with

; ACL2 !>:brr t

; and then install an unconditional monitor on the rewrite rule
; `dupsp-append`, whose rune is (:REWRITE DUPSP-APPEND), with:

; :monitor (:rewrite dupsp-append) t

; Then we could re-try our main theorem, dupsp-rev.  At the resulting
; interactive break we type :eval to evaluate the attempt to relieve the
; hypotheses of the rule.

; (1 Breaking (:REWRITE DUPSP-APPEND) on
; (DUPSP (BINARY-APPEND (REV #) (CONS # #))):
; 1 ACL2 >:eval

; 1x (:REWRITE DUPSP-APPEND) failed because :HYP 1 rewrote to
; (NOT (MEMBER (CAR X) (REV #))).

; Note that the report above shows that hypothesis 1 of the rule
; did not rewrite to T but instead rewrote to an expression
; involving `(member ... (rev ...))`.  Thus, we're led to the
; same conclusion that Thinking produced.  To get out of the
; interactive break we type:

; 1 ACL2 >:a!
; Abort to ACL2 top-level

; and then turn off the break rewrite tool since we won't need it
; again right now, with:

; ACL2 !>:brr nil

; In either case, by thinking or using tools, we decide to prove:

(defthm member-rev
(iff (member e (rev x))
(member e x)))

; which succeeds.  Now when we try to prove dups-rev, it succeeds.

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

```