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 on Several Variables To (p n x) for all n and all x,
prove each of the following:
Base Case 1:
(implies (endp x)
(p n x))
Base Case 2:
(implies (and (not (endp x))
(zp n))
(p n x))
Induction Step:
(implies (and (not (endp x))
(not (zp n))
(p (- n 1) (cdr x)))
(p n x))
A function that suggests this induction is
(defun nth (n x)
(if (endp x)
nil
(if (zp n)
(car x)
(nth (- n 1) (cdr x))))).
