### SOLUTION-TO-SIMPLE-EXAMPLE

solution to a simple example
```Major Section:  TUTORIAL-EXAMPLES
```

To see a statement of the problem solved below, see tutorial-examples.

Here is a sequence of ACL2 events that illustrates the use of ACL2 to make definitions and prove theorems. We will introduce the notion of the fringe of a tree, as well as the notion of a leaf of a tree, and then prove that the members of the fringe are exactly the leaves.

We begin by defining the fringe of a tree, where we identify trees simply as cons structures, with atoms at the leaves. The definition is recursive, breaking into two cases. If `x` is a cons, then the `fringe` of `x` is obtained by appending together the `fringe`s of the `car` and `cdr` (left and right child) of `x`. Otherwise, `x` is an atom and its `fringe` is the one-element list containing only `x`.

```

(defun fringe (x)
(if (consp x)
(append (fringe (car x))
(fringe (cdr x)))
(list x)))

```
Now that `fringe` has been defined, let us proceed by defining the notion of an atom appearing as a ``leaf'', with the goal of proving that the leaves of a tree are exactly the members of its `fringe`.
```

(defun leaf-p (atm x)
(if (consp x)
(or (leaf-p atm (car x))
(leaf-p atm (cdr x)))
(equal atm x)))

```
The main theorem is now as follows. Note that the rewrite rule below uses the equivalence relation `iff` (see equivalence) rather than `equal`, since `member` returns the tail of the given list that begins with the indicated member, rather than returning a Boolean. (Use `:pe member` to see the definition of `member`.)
```

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

```