- Def: CP (s, t) zusammenführbar,
falls
∃u : s→R*u∧t→R*u.
- Wenn
SN(R), dann ist Zusammenführbarkeit entscheidbar
- Wenn R endlich, dann hat R endlich viele CP.
-
WCR(R) gdw. jedes kritische Paar zusammenführbar.
- Satz: Für endliche terminierende R ist Konfluenz entscheidbar.
