## TUTORIAL-EXAMPLES

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

Beginning users may find these examples at least as useful as the extensive documentation on particular topics. 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
```
You may also wish to visit the other introductory sections, startup and tidbits. These contain further information related to the use of ACL2.

• ### TUTORIAL5-MISCELLANEOUS-EXAMPLES -- miscellaneous ACL2 examples

When you feel you have read enough examples, you might want to try the following very simple example on your own. 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))))

```
For a solution, see solution-to-simple-example.