### 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)))).