La confluence d'un système de réécriture
Pour tous termes M,M1,M2 tels que
La confluence est trivialement équivalente à la propriété de Church-Rosser.
Le lemme de Newmann énonce qu'un système de réécriture terminant et localement confluent est confluent.
La propriété du diamant implique aussi la confluence du système.