### EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION

induction on natural numbers
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 Natural Numbers**: Induction is familiar in the
arithmetic setting. To prove `(p n)`

, for all `n`

, by classical
induction on the construction of the natural numbers, prove each of the
following:

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

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

The Base Case establishes that `p`

holds for `0`

. In fact, because of
the definition of `zp`

, it establishes that `(p n)`

holds when
`n`

is `0`

and it holds when `n`

is not a natural number.
The Induction Step establishes that if `n`

is a natural number other than `0`

,
and if `p`

holds for `n`

-1, then `p`

holds for `n`

. The hypothesis
`(p (- n 1))`

above is called the *induction hypothesis*.

A function that suggests this induction is

(defun nat-recursion (n)
(if (zp n)
n
(nat-recursion (- n 1))))

Similarly, the term `(fact n)`

suggests this induction if `fact`

is defined:
(defun fact (k)
(if (zp k)
1
(* k (fact (- k 1))))).

even though the formal parameter of this definition of `fact`

is `k`

, not `n`

.