# LP, the Larch Prover -- Reduction

Terms can be *reduced* or *rewritten* by the application of a
rewrite rule, as follows. First, the left side of the
rewrite rule is matched against the term or one of its subterms.
(Matching is the process of finding a
substitution for the variables of a term
that makes it equivalent to another term.) If matching is successful, the
resulting substitution is applied to the right side of the rewrite rule and the
matched term is replaced with this new term.