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
by classical induction on binary tree structures, prove each of the
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))))).