		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Example-induction-scheme-down-by-2

Induction downwards 2 steps at a time

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 Natural Numbers Preserving Parity: Here is another way to decompose natural numbers. To prove (p n), for all n, prove each of the following:

Base Case 1: 
(implies (zp n) (p n))

Base Case 2: 
(implies (equal n 1) (p n))

Induction Step: 
(implies (and (not (zp n)) 
              (not (equal n 1)) 
              (p (- n 2))) 
         (p n))

Base Case 1 establishes that p holds for 0 (and all objects other than positive naturals).

Base Case 2 establishes that p holds for 1.

The Induction Step establishes that if n is a natural number greater than 1, and if p holds for n-2, then p holds for n.

Note that we have thus proved that (p n) holds, for all n. For example, (p -7), (p 'abc), and (p 0) are all established by Base Case 1. (p 1) is established by Base Case 2. (p 2) is established from (p 0) and the Induction Step. Think about it! (p 3) is established form (p 1) and the Induction Step, etc.

A function that suggests this induction is:

(defun parity (n)
  (if (zp n)
      'even
      (if (equal n 1)
          'odd
          (parity (- n 2))))).