Diagram Techniques for Confluence


We develop diagram techniques for proving confluence in abstract reduction systems. theory gives a systematic and uniform framework in which a number of known results, widely scattered throughout the literature, can be understood. These results include Newman's Lemma (1942), Lemma 3.1 of Winkler and Buchberger (1985), the Hindley-Rosen Lemma (1964), the Request Lemma of Staples (1975), the Strong Confluence Lemma of Huet (1980), and the Lemma of De Bruijn (1978).