\begin{frame}
  \small

  \begin{definition}[Overlining]
  For a TRS $\atrs = \langle \Sigma,R \rangle$ we define the
  \alert{overlined} TRS $\overline{\atrs} = \langle \overline{\Sigma},\overline{R} \rangle$:
  \begin{itemize}
    \item $\overline{\Sigma} = \Sigma \cup \{\overline{f} \mid f\in\Sigma\}$,
    \item $\overline{R} = \{\overline{\rho} \mid \rho \in R\}$
  \end{itemize}
  where 
  $\overline{\rho}$ is obtained from $\rho$ by overlining the head symbol of the left-hand side.
  \begin{center}
  $\rho : f(s_1,\ldots,s_n) \to r$ \quad yields \quad
  $\overline{\rho} : \overline{f}(s_1,\ldots,s_n) \to r$
  \end{center}
  \smallskip
  \end{definition}
  \medskip\pause

  \begin{example}
  The overlined version of Combinatory Logic:
  \begin{center}
  \(
  \begin{array}{lcl}
  \rule[1ex]{0ex}{2ex}
  \overline{Ap}(Ap(Ap (S,x),y),z) & \to & Ap(Ap(x,z), Ap(y,z))\\
  \overline{Ap}(Ap(K,x),y)&\to&  x\\
  \overline{Ap} (I,x)&\to&  x
  \rule[-2ex]{0ex}{2ex}
  \end{array}\)
  \end{center}
  \end{example}
\end{frame}