Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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

(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x))))); Trying

`triple-rev`

at this point produces a key checkpoint containing ;`(REV (APPEND (REV (CDR X)) (LIST (CAR X))))`

, which suggests:(defthm rev-append (equal (rev (append a b)) (append (rev b) (rev a))))

; And now

`triple-rev`

succeeds.(defthm triple-rev (equal (rev (rev (rev x))) (rev x)))

; An alternative, and more elegant, solution is to prove the

`rev-rev`

; instead of`rev-append`

:; (defthm rev-rev ; (implies (true-listp x) ; (equal (rev (rev x)) x)))

;

`Rev-rev`

is also discoverable by The Method because it is ; suggested by the statement of`triple-rev`

itself:`rev-rev`

; simplifies a simpler composition of the functions in`triple-rev`

.; Both solutions produce lemmas likely to be of use in future proofs ; about

`rev`

.

Use your browser's **Back Button** now to return to
introductory-challenge-problem-1.