Kritische Paare

Def: Für ein Termersetzungssystem R über Σ: falls

(l₁→r₁) und (l₂→r₂) sind Regeln in R ohne gemeinsame Variable (ggf. vorher umbenennen!)
es gibt p∈Pos(l₁), so daß l₁[p] $\notin$ Var und
l₁[p] und l₂ sind unifizierbar mit mgu σ, d.h., l₁[p]σ = l₂σ
falls (l₁→r₁) = (l₂→r₂) (vor Umbenennung), dann p≠ε
dann ist (r₁σ,(l₁σ)[p : = r₂σ]) kritisches Paar (CP) von R.

Bsp: {f (f (x, y), z)→₁f (x, f (y, z)), f (i(x), x)→₂e()}