### 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)).