Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Here are some pages illustrating various induction schemes suggested by recursive functions.

**Classical Induction on Natural Numbers**:
see example-induction-scheme-nat-recursion.

**Induction Preserving Even/Odd Parity** or

**Induction Downwards by 2** or

**Induction with Multiple Base Cases**:
see example-induction-scheme-down-by-2 for an induction in which the
induction hypothesis decreases the induction variable by an amount other
than 1. This illustrates that the induction hypothesis can be about
whatever term or terms are needed to explain how the formula recurs. The
example also illustrates an induction with more than one Base Case.

**Classical Induction on Lists**:
see example-induction-scheme-on-lists for an induction over linear lists,
in which we inductively assume the conjecture for `(cdr x)`

and prove it
for `x`

. It doesn't matter whether the list is `nil`

-terminated or not;
the Base Case addresses all the possibilities.

**Classical Induction on Binary (Cons) Trees**:
see example-induction-scheme-binary-trees for an induction over the simplest
form of binary tree. Here the Induction Step provides two hypotheses, one
about the left subtree and one about the right subtree.

**Induction on Several Variables**:
see example-induction-scheme-on-several-variables for an induction in which
several variables participate in the case analysis and induction hypotheses.

**Induction Upwards**:
see example-induction-scheme-upwards for an induction scheme in which
the induction hypothesis is about something ``bigger than'' the induction conclusion.
This illustrates that the sense in which the hypothesis is about something ``smaller''
than the conclusion is determined by a measure of all the variables, not the magnitude
or extent of some single variable.

**Induction with Auxiliary Variables** or

**Induction with Accumulators**:
see example-induction-scheme-with-accumulators for an induction scheme in which
one variable ``gets smaller'' but another is completely arbitrary. Such schemes
are common when dealing with tail-recursive functions that accumulate partial
results in auxiliary variables. This example also shows how to provide
several arbitrary terms in a non-inductive variable of a scheme.

**Induction with Multiple Induction Steps**:
see example-induction-scheme-with-multiple-induction-steps for an induction in
which we make different inductive hypotheses depending on which case we're in.
This example also illustrates the handling of auxiliary variables or
accumulators.