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.