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.
Classical Induction on Lists: To prove
(p x), for all
classical induction on the linear list structure, prove each of the
Base Case: (implies (endp x) (p x))
Induction Step: (implies (and (not (endp x)) (p (cdr x))) (p x))
An argument analogous to that given for natural numbers,
(p x) for every
x. For example,
(p 'abc), and
(p nil) are all
established by the Base Case.
(p '(Friday)) follows from
given the Induction Step. That sentence bears thinking about! Think about
(p '(Yellow)) holds for the same reason.
(p '(Thursday Friday)) follows from
(p '(Friday)) and the Induction Step,
A function that suggests this induction is
(defun app (x y) (if (endp x) y (cons (car x) (app (cdr x) y)))).