# Induction-schemes

A variety of basic, widely applicable induction schemes.

The definitions here are meant to be used in induct hints or
as the :scheme for induction rules. You would typically include
them only locally, e.g., with:

(local (include-book "std/basic/inductions" :dir :system))

For general background on induction schemes, see logic-knowledge-taken-for-granted-inductive-proof and example-inductions.

### Subtopics

- Dec-dec-induct
`(dec-dec-induct n m)` inducts by simultaneously subtracting
1 each from n and m, until either one reaches 0.- Cdr-dec-induct
`(cdr-dec-induct x n)` inducts by simultaneously cdr'ing
x and subtracting 1 from n, until we reach the end of x or
n reaches 0.- Cdr-cdr-induct
`(cdr-cdr-induct x y)` inducts by simultaneously cdr'ing
x and y until we reach the end of either.- Dec-induct
`(dec-induct n)` is classic natural-number induction on n;
we just subtract 1 until reaching 0.- Cdr-induct
`(cdr-induct x)` is classic list induction, i.e., cdr
until you reach the end of the list.