A few simple checkpoints suggesting strong rules
Consider these definitions:
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x))))) (defun nats-below (j) (if (zp j) '(0) (cons j (nats-below (- j 1)))))
We assume you are familiar with such ACL2 built-ins as
Below are some terms that should suggest rewrite rules to you. Imagine that each of these terms occurs in some Key Checkpoint. What rules come to mind? Try to think of the strongest rules you can.
Answers: See practice-formulating-strong-rules-1
Answers: See practice-formulating-strong-rules-2
Answers: See practice-formulating-strong-rules-3
Answers: See practice-formulating-strong-rules-4
Answers: See practice-formulating-strong-rules-5
Answers: See practice-formulating-strong-rules-6
We recommend doing all of these little exercises. When you're finished, use your browser's Back Button to return to strong-rewrite-rules.