Confluencia (Propiedad de Church–Rosser)

Propiedad de un sistema de reescritura o reducción que afirma que siempre que un término puede reducirse por dos secuencias (posiblemente distintas) a términos s y t, existe un término u al que tanto s como t pueden reducirse ulteriormente (es decir, s ↓ u y t ↓ u). La confluencia suele llamarse propiedad de Church–Rosser.