  In this paper we give a criterion by which one can conclude that every
reduction of a basic term to normal form has the same length. As a consequence,
the number of steps to reach the normal form is independent of the chosen
strategy. In particular this holds for TRSs computing addition and
multiplication of natural numbers, both in unary and binary notation.

Logic in Computer Science;Programming Languages