EXAMPLE-INDUCTION-SCHEME-WITH-MULTIPLE-INDUCTION-STEPS

induction scheme with more than one induction step
```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.

Several Induction Steps: To `(p x i a)` for all `x`, `i`, and `a`, prove each of the following:

```Base Case 1:
(implies (zp i)
(p x i a))
```

```Induction Step 1:
(implies (and (not (zp i))
(equal (parity i) 'even)
(p (* x x)
(floor i 2)
a))
(p x i a))
```

```Induction Step 2:
(implies (and (not (zp i))
(not (equal (parity i) 'even))
(p x
(- i 1)
(* x a)))
(p x i a))
```

A function that suggests this induction is the binary exponentiation function for natural numbers.

```(defun bexpt (x i a)
(cond ((zp i) a)
((equal (parity i) 'even)
(bexpt (* x x)
(floor i 2)
a))
(t (bexpt x
(- i 1)
(* x a)
)))).
```
In order to admit this function it is necessary to know that `(floor i 2)` is smaller than `i` in the case above. This can be proved if the book `"arithmetic-5/top"` has been included from the ACL2 system directory, i.e.,
```(include-book "arithmetic-5/top" :dir :system)
```
should be executed before defining `bexpt`.