Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

International audienceUser-de ned higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. is raises the question of proving that they preserve the properties of β-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom's decreasing diagrams that reduce con uence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, con uence of a terminating set of le-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. e present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pars. e rewrite relation used for analyzing con uence, called orthogonal, gives rise to critical pairs, called nested, that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. is second paper terminates our investigation of con uence in the case of le-linear rules