Eine zweistellige Relation ρ heißt lokal konfluent, wenn ∀x, y1, y2 : ρ(x, y1)∧ρ(x, y2)⇒∃z : ρ*(y1, z)∧ρ*(y2, z)
lokale Konfluenz erkennt man durch Betrachtung von Überlappungen von linken Regelseiten.
diese (Teilterme der) linke Seiten enthalten Variablen, deswegen muß man unifizieren.