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
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
iin 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