Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Start in a fresh ACL2, either by restarting your ACL2 image from scratch or executing
:ubt! 1which will undo everything since the first user event.
Then define this function:
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))Then use The Method to prove:
(defthm triple-rev (equal (rev (rev (rev x))) (rev x)))
When you've solved this problem, compare your answer to ours; see introductory-challenge-problem-1-answer.
Then, use your browser's Back Button to return to introductory-challenges.