Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs

In a series of papers, we develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending β-reduction on pure λ-terms. The present paper concentrates on the case of left-linear rewrite rules, assuming that critical pairs can be joined without explicit beta-reduction steps