# LP, the Larch Prover -- Induction rules

An *induction rule* is logically equivalent to an infinite set of formulas,
which justify the use of proofs by induction.
`<induction-rule> ::= ``sort` <sort> `generated` [ `freely` ] `by` <operator>+,
| `well founded` <operator>

## Examples

`sort Nat generated freely by 0, s
sort Set generated by {}, insert
sort Set generated by {}, {__}, \U
well founded <
`

## Usage

Users can assert or prove induction rules.
Assertions like `sort Nat generated by 0, s` specify sets of generators for
use in proofs by structural induction. The
listed operators (e.g, `0` and `s`) must have the named sort (e.g.,
`Nat`) as their range. If none of the domain sorts of an operator is the
same as its range sort, the operator is a *basis generator* (e.g., `0`);
otherwise, it is an *inductive generator* (e.g, `s`). Structural
induction rules are logically equivalent to infinite sets of first-order
formulas of the form

`P(0) /\ \A x (P(x) => P(s(x))) => \A x P(x)
`

where `P` is an arbitrary first-order formula.
The use of `freely` supplements a structural induction rule with a set of
formulas asserting that the named operators are one-to-one and have disjoint
ranges. For example, `sort Nat generated freely by 0, s` gives rise to the
formulas `s(x) = s(y) <=> x = y` and `0 ~= s(x)`.

Assertions like `well founded <` specify a binary relation for use in
proofs by well-founded induction. The listed
operator must have a signature of the form `S,S->Bool` for some sort `S`.
Well-founded induction rules are logically equivalent to infinite sets of
first-order formulas of the form

`\A x (\A y (y < x => P(y)) => P(x)) => \A x P(x)
`

where `P` is an arbitrary first-order formula.
To display the induction rules that LP currently has available for use,
type `display induction-rules` (or `disp i-r` for short).