\begin{slide}{Regeln}

\begin{itemize}
\item
  Regel $(l,r)$, Schreibweise $(l \to r)$, mit $l,r\in \Term(\Sigma,V)$
\item
  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]$
\end{itemize}

  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)))$.

\end{slide}
