Induction downwards 2 steps at a time
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 Preserving Parity: Here is
another way to decompose natural numbers. To prove
Base Case 1: (implies (zp n) (p n))
Base Case 2: (implies (equal n 1) (p n))
Induction Step: (implies (and (not (zp n)) (not (equal n 1)) (p (- n 2))) (p n))
Base Case 1 establishes that
Base Case 2 establishes that
The Induction Step establishes that if
Note that we have thus proved that
A function that suggests this induction is:
(defun parity (n) (if (zp n) 'even (if (equal n 1) 'odd (parity (- n 2))))).