# Confluence by Critical Pair Analysis Revisited (Extended Version)

## TL;DR

This paper introduces two novel methods for proving confluence in left-linear term rewrite systems, leveraging rule labelling and critical pair analysis to simplify the confluence verification process.

## Contribution

It revisits and extends the critical pair analysis approach, proposing hot-decreasingness and critical-pair-closing system methods for improved confluence proofs.

## Key findings

- Both methods effectively prove confluence in complex systems.
- The approaches unify existing theorems with new rule labelling techniques.
- Experimental results demonstrate their applicability to a range of rewrite systems.

## Abstract

We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.