Some examples of induction schemes in ACL2

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

**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.