# LP, the Larch Prover -- Rewrite rules

A *rewrite rule* is an operational form for a formula. LP uses rewrite
rules to rewrite terms to logically equivalent terms.
`<rewrite-rule> ::= <term> ``->` <term>

Restrictions: The two <term>s in a rewrite rule must have the same sort. The
left side of the rule must not be a variable, the logical constant `true`,
or the logical constant `false`. Every free variable in the right side must
also occur free in left side.
## Examples

`x + 0 -> x
x <= y -> x < y \/ x = y
x | y -> \E z (y = x*z)
0 < 1 -> true
`

## Usage

Users cannot assert or prove rewrite rules directly. Instead,
they must assert or prove formulas, which LP then
orients into rewrite rules. The logical content
of a term is the equation that results from replacing `->` by `=`.
LP maintains the invariant that all active
rewrite rules have been applied to all nonimmune
formulas, rewrite rules, and deduction rules in the system.

Some rewrite rules are hardwired into LP to define properties of the
logical connectives, the conditional
and equality operators, and the
quantifiers.

The restriction that the left side of a rewrite rule not be a variable prevents
``rules'' like `x -> f(x)` from leading to a nonterminating rewriting
sequence such as `x -> f(x) -> f(f(x)) -> ...`. The restriction that it not
be `true` or `false` preserves the meaning of those logical constants.
The restriction that the right side not introduce a free variable is more
technical. It prevents logically equivalent ``rules'' such as
`f(x) -> f(y)` and `f(u) -> f(v)` from producing different results when
applied to terms like `y + f(x)`.