### INTRODUCTORY-CHALLENGES

challenge problems for the new ACL2 user
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Do each of the problems. In each case, start with a fresh ACL2 (or undo all effects of
previous events with `:ubt! 1`

). This may require that you ``re-discover'' the same
lemma more than once in different problems, but recognizing the need for something you
used in some previous project is part of the training.

We recommend that you follow The Method and consult the documentation as
needed -- but that you not look at our answers until you're well and truly
baffled!

See introductory-challenge-problem-1 (Answer: introductory-challenge-problem-1-answer)

See introductory-challenge-problem-2 (Answer: introductory-challenge-problem-2-answer)

See introductory-challenge-problem-3 (Answer: introductory-challenge-problem-3-answer)

See introductory-challenge-problem-4 (Answer: introductory-challenge-problem-4-answer)

In addition to these explicit challenge problems designed for beginners, the ACL2
documentation has many example solutions to problems (not always phrased in the
question/answer format here). If you are looking for other examples, you should
consider

annotated-acl2-scripts (Answer: the answers are given in the examples)

When you've done the problems and compared your solutions to ours, use your
browser's **Back Button** now to return to
introduction-to-the-theorem-prover.