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

.