## ANNOTATED-ACL2-SCRIPTS

examples of ACL2 scripts
```Major Section:  ACL2-TUTORIAL
```

Beginning users may find these annotated scripts useful. We suggest that you read these in the following order:

```Tutorial1-Towers-of-Hanoi
Tutorial2-Eights-Problem
Tutorial3-Phonebook-Example
Tutorial4-Defun-Sk-Example
Tutorial5-Miscellaneous-Examples
```

The page http://www.cs.utexas.edu/users/moore/publications/tutorial/rev3.html contains a script that illustrates how it feels to use The Method to prove an unusual list reverse function correct. The screen shots of ACL2's proof output are outdated -- in the version shown, ACL2 does not print Key Checkpoints, but the concept of key checkpoint is clear in the discussion and the behavior of the user.

At http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/index.html is the demo given by Matt Kaufmann at TPHOLs08, including all the scripts. There is a gzipped tar file containing the entire contents of the demos.

At http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence is a collection of scripts illustrating both high-level strategy and lower-level tactics dealing with the functional equivalence of various list sorting algorithms. Start with the `README` on that directory. There is also a gzipped tar file containing all the scripts, at http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence.tgz.

When you feel you have read enough examples, you might want to try the following very simple example on your own. (See solution-to-simple-example for a solution, after you work on this example.) First define the notion of the ``fringe'' of a tree, where we identify trees simply as cons structures, with atoms at the leaves. For example:

```

ACL2 !>(fringe '((a . b) c . d))
(A B C D)

```
Next, define the notion of a ``leaf'' of a tree, i.e., a predicate `leaf-p` that is true of an atom if and only if that atom appears at the tip of the tree. Define this notion without referencing the function `fringe`. Finally, prove the following theorem, whose proof may well be automatic (i.e., not require any lemmas).
```

(defthm leaf-p-iff-member-fringe
(iff (leaf-p atm x)
(member-equal atm (fringe x))))

```