Bsp. Kritische Paare für SRS

• E₀ = {aba→ε}, als TRS: {a(b(a(x)))→x}
• Überlappung der Regel mit sich an Position [0, 0]

  l₁ = aba(x), r₁ = x, l₂ = aba(x'), r₂ = x', p = [0, 0]

  l₁[p] = a(x), mgu(l₁[p], l₂) = {x $\mapsto$ ba(x')} = σ

  das aus dieser Überlappung konstruierte CP ist

  (r₁σ,(l₁σ)[p : = r₂σ]) = (xσ,(aba(x)σ)[p : = x'σ]) = (ba(x'), ababa(y)[p : = x']) = (ba(x'), ab(x'))

• Ü: alle CP für E₁ = E₀∪{ba(x')→ab(x')}
• Ü: alle CP für {aba(x)→b(x)}