### EXAMPLE-INDUCTION-SCHEME-UPWARDS

induction upwards
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.

**Induction Upwards**: To `(p i max)`

for all `i`

and all `max`

,
prove each of the following:

*Base Case*:
(implies (not (and (natp i)
(natp max)
(< i max)))
(p i max))

*Induction Step*:
(implies (and (natp i)
(natp max)
(< i max)
(p (+ i 1) max))
(p i max))

Note that the induction hypothesis is about an `i`

that is *bigger* than
the `i`

in in the conclusion. In induction, as in recursion, the sense of
one thing being ``smaller'' than another is determined by an arbitrary
measure of all the variables, not the magnitude or extent of some particular
variable.A function that suggests this induction is shown below. ACL2 has to be told
the measure, namely the difference between `max`

and `i`

(coerced to a natural
number to insure that the measure is an ordinal).

(defun count-up (i max)
(declare (xargs :measure (nfix (- max i))))
(if (and (natp i)
(natp max)
(< i max))
(cons i (count-up (+ 1 i) max))
nil)).