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-revat 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-revsucceeds. (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-revis also discoverable by The Method because it is ; suggested by the statement of
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
Use your browser's Back Button now to return to introductory-challenge-problem-1.