214/365
\begin{frame}
  \frametitle{Dependency Pairs}
  
  For every $f \in \Sigma$ let $f_\#$ be a fresh symbol with the same arity as $f$.\\
  \pause
  By $t_\#$ we denote $f_\#(t_1,\dots,t_n)$ for $t = f(t_1,\dots,t_n) \in \TTlong$.
  \pause\medskip
  
  \begin{definition}[Dependency Pairs]
  \centerline{$\DP(R) = \{\ell_\# \to r'_\# \mid \ell \to r \in R,\; r' \trianglelefteq r \text{ with } r' \not\in {\cal X}\}$}
  \end{definition}\ \\[-.8em]
  \pause\medskip
  
  \begin{example}
  \vspace{-1em}
  \begin{align*}
  R = \{ \; {\rm f}(x) \to {\rm g}({\rm f}(x)) \;\}
  \end{align*}
  \pause\vspace{-3em}
  
  \begin{align*}
  \DP(R) = \{\;
    {\rm f}_\#(x) &\to {\rm g}_\#({\rm f}(x)),\\
    {\rm f}_\#(x) &\to {\rm f}_\#(x)
  \;\}
  \end{align*}
  \vspace{-1.5em}
  \end{example}
\end{frame}