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