Induction on natural numbers
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.
Classical Induction on Natural Numbers: Induction is familiar in the
arithmetic setting. To prove
Base Case: (implies (zp n) (p n))
Induction Step: (implies (and (not (zp n)) (p (- n 1))) (p n))
The Base Case establishes that
The Induction Step establishes that if
A function that suggests this induction is
(defun nat-recursion (n) (if (zp n) n (nat-recursion (- n 1))))
Similarly, the term
(defun fact (k) (if (zp k) 1 (* k (fact (- k 1))))).
even though the formal parameter of this definition of