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-ExamplesYou may also wish to visit the other introductory sections, startup and tidbits. These contain further information related to the use of ACL2.

### SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example

### TUTORIAL1-TOWERS-OF-HANOI -- The Towers of Hanoi Example

### TUTORIAL2-EIGHTS-PROBLEM -- The Eights Problem Example

### TUTORIAL3-PHONEBOOK-EXAMPLE -- A Phonebook Specification

### TUTORIAL4-DEFUN-SK-EXAMPLE -- example of quantified notions

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

Next, define the notion of a ``leaf'' of a tree, i.e., a predicateACL2 !>(fringe '((a . b) c . d)) (A B C D)

`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).
For a solution, see solution-to-simple-example.(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))