### EXAMPLE-INDUCTION-SCHEME-ON-LISTS

induction on lists
```Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER
```

See logic-knowledge-taken-for-granted-inductive-proof for an explanation of what we mean by the induction suggested by a recursive function or a term.

Classical Induction on Lists: To prove `(p x)`, for all `x`, by classical induction on the linear list structure, prove each of the following:

```Base Case:
(implies (endp x) (p x))
```

```Induction Step:
(implies (and (not (endp x))
(p (cdr x)))
(p x))
```

An argument analogous to that given for natural numbers, example-induction-scheme-nat-recursion, establishes `(p x)` for every `x`. For example, `(p -7)`, `(p 'abc)`, and `(p nil)` are all established by the Base Case. `(p '(Friday))` follows from `(p nil)`, given the Induction Step. That sentence bears thinking about! Think about it! Similarly, `(p '(Yellow))` holds for the same reason. `(p '(Thursday Friday))` follows from `(p '(Friday))` and the Induction Step, etc.

A function that suggests this induction is

```(defun app (x y)
(if (endp x)
y
(cons (car x)
(app (cdr x) y)))).
```