### EXAMPLE-INDUCTION-SCHEME-ON-SEVERAL-VARIABLES

induction on several variables
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))))).