LP, the Larch Prover -- Convergence

A set of rewrite rules is called convergent if all terms can be rewritten to a terminal form in a finite number of steps, and all terms have a unique normal form.

See also