- für eine Relation → auf U: das Element x∈U heißt ...
- terminierend,
SN(x): es gibt keine unendliche Kette,
die bei x beginnt:
x = x0→x1→...
- normalisierend,
WN(x): x hat Normalform
- hat Diamant-Eigenschaft,
DP(x): wenn
∀y1, y2 : y1←x→y2 : ∃z : y1→z←y2
- lokal konfluent,
WCR(x):
wenn
∀y1, y2 : y1←x→y2 : y1↓y2
- konfluent,
CR(x):
wenn
∀y1, y2 : y1←*x→*y2 : y1↓y2
- Beispiele, trennende Beispiele
- normalisierend, aber nicht terminierend
- lokal konfluent, aber nicht konfluent
