### 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`.