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.