### EXAMPLE-INDUCTION-SCHEME-BINARY-TREES

induction on binary trees
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 Binary Trees**: To prove `(p x)`

, for all `x`

,
by classical induction on binary tree structures, prove each of the
following:

*Base Case*:
(implies (atom x) (p x))

*Induction Step*:
(implies (and (not (atom x))
(p (car x))
(p (cdr x)))
(p x))

An argument analogous to that given in example-induction-scheme-on-lists
should convince you that `(p x)`

holds for every object.

A function that suggests this induction is:

(defun flatten (x)
(if (atom x)
(list x)
(app (flatten (car x))
(flatten (cdr x))))).