### EXAMPLE-INDUCTION-SCHEME-DOWN-BY-2

induction downwards 2 steps at a time
```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 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))))).
```