		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Example-induction-scheme-on-lists

Induction on lists

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