EXAMPLE-INDUCTION-SCHEME-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))))).