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.
Next, define the notion of a ``leaf'' of a tree, i.e., a predicate
ACL2 !>(fringe '((a . b) c . d)) (A B C D)
leaf-pthat 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))))