Regeln

• Regel (l, r), Schreibweise (l$\to$r), mit l, r $\in$ Term($\Sigma$, V)
• Regel (l$\to$r) an Position p in t $\in$ Term($\Sigma$) anwenden, um s zu erhalten, Schreibweise t$\to_{{(l\to r),p}}^{}$s

  $\exists$$\sigma$ : V$\to$Term($\Sigma$) : t|_p = l$\sigma$ $\wedge$ s = t[p : = r$\sigma$]

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

Position p = [2] $\in$ Pos(t), Teilterm t|_p = f (f (2)),

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

auf r anwenden: r$\sigma$ = g(f (2), f (2)),

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