\doc{Termination}
\ref{termination}
\ref{terminating}

A set of \llink{rewrite-rule}{rewrite rules} is called \def{terminating} if
each term can be \olink{reduce}{reduced} only a finite number of times.
Generally some well-founded ordering on terms is used to establish the
termination of a rewriting system.