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 = [1]∈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))).