Regeln

• Regel (l, r) , Schreibweise (l→r) , mit l, r∈Term(Σ, V)
• Regel (l→r) an Position p in t∈Term(Σ) anwenden, um s zu erhalten, Schreibweise t→_{(l→r), p}s

  ∃σ : V→Term(Σ) : t|_p = lσ∧t[p : = rσ] = s

Beispiel: Regel (l, r) = (f (x), g(x, x)) , Term t = h(1, f (f (2))) .

Position p = [2]∈Pos(t) , Teilterm t|_p = f (f (2)) ,

Substitution σ : x $\mapsto$ f (2) mit t|_p = lσ ,

auf r anwenden: rσ = g(f (2), f (2)) ,

in t einsetzen: s = t[p : = rσ] = h(1, rσ) = h(1, g(f (2), f (2))) .