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
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
A function that suggests this induction is shown below. ACL2 has to be
told the measure, namely the difference between
(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)).