Induction scheme with more than one induction step
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
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
(include-book "arithmetic-5/top" :dir :system)
should be executed before defining