Orthogonale Systeme

• ein TRS R über Σ heißt nichtüberlappend, wenn R keine kritischen Paare besitzt.

  (dann gilt WCR(R) trivialerweise)

• ein TRS R heißt linkslinear, wenn in keiner linken Regelseite eine Variable mehrfach vorkommt.
• ein TRS R heißt orthogonal, falls es linkslinear und nichtüberlappend ist.
• Satz: jedes orthogonale System ist konfluent.

  beachte: das gilt auch für nicht-terminierende Systeme

• braucht man linkslinear wirklich? Ja:

  {f (x, x)→a, f (x, g(x))→b, c→g(c)}