\begin{frame}
\frametitle{Dependency Pairs, Examples}

\begin{example}
\vspace{-1em}
\begin{align*}
R = \{ \; {\rm f}({\rm g}(x)) &\to {\rm g}({\rm g}({\rm f}({\rm f}(x)))) \;\}
\end{align*}
\vspace{-3.5em}

\pause
\begin{align*}
\DP(R) = \{\;
  {\rm f}_\#({\rm g}(x)) &\to {\rm g}_\#({\rm g}({\rm f}({\rm f}(x)))),\\
  {\rm f}_\#({\rm g}(x)) &\to {\rm g}_\#({\rm f}({\rm f}(x))),\\
  {\rm f}_\#({\rm g}(x)) &\to {\rm f}_\#({\rm f}(x)),\\
  {\rm f}_\#({\rm g}(x)) &\to {\rm f}_\#(x)
\;\}
\end{align*}
\vspace{-1.5em}

\pause
$R$ is non-terminating:
\vspace{-.5em}
\begin{align*}
  {\rm \alert{f}}({\rm \alert{g}}({\rm g}(x)))
  \to {\rm g}({\rm g}({\rm f}({\rm \alert{f}}({\rm \alert{g}}(x)))))
  \to {\rm g}({\rm g}({\rm \emph{f}}({\rm \emph{g}}({\rm \emph{g}}({\rm f}({\rm f}(x)))))))
  \to \ldots
\end{align*}
\vspace{-1.5em}

\pause
How does an infinite $\to_R \cup \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)}$ rewrite sequence look like?
\pause
\vspace{-.5em}
\begin{align*}
  {\rm \alert{f_\#}}({\rm \alert{g}}({\rm g}(x)))
  \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)}
    {\rm f}_\#({\rm \alert{f}}({\rm \alert{g}}(x)))
  \to_R {\rm \emph{f_\#}}({\rm \emph{g}}({\rm \emph{g}}({\rm f}({\rm f}(x))))
  \to \ldots
\end{align*}
\vspace{-1.5em}

\end{example}

\end{frame}