Strategy Independent Reduction Lengths in Rewriting and Binary Arithmetic

Hans Zantema

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…