		Search-engine friendly clone of the ACL2 documentation.

Example-induction-scheme-binary-trees

Induction on binary trees

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