\begin{frame}[t]
  \frametitle{Dependency Graphs}
  
  \vspace{-1em}
  \begin{example}
  \vspace{-1em}
  \begin{align*}
  \minus(x,0) &\to x\\
  \minus(\s(x),\s(y)) &\to \minus(x,y)\\
  \quot(0,\s(y)) &\to 0\\
  \quot(\s(x),\s(y)) &\to \s(\quot(\minus(x,y),\s(y)))
  \end{align*}
  \vspace{-1em}
  \pause

  Dependency graph: analysis which DP-rules may follow each other
  \vspace{-.5em}
  \begin{center}
    \begin{tikzpicture}
      \begin{scope}[node distance=5mm,very thick]
      \node (m) {(1) $\minus_\#(\s(x),\s(y)) \to \minus_\#(x,y)$};
      \node (qm) [below=of m] {(2) $\quot_\#(\s(x),\s(y)) \to \minus_\#(x,y)$};
      \node (qqm) [below=of qm] {(3) $\quot_\#(\s(x),\s(y)) \to \quot_\#(\minus(x,y),\s(y))$};
      \draw[->] (qm) -- (m);
      \draw[->] (qqm) -- (qm);
      \draw[->] (qqm) to[out=-4,in=4,looseness=2.5] (qqm);
      \draw[->] (m) to[out=-4,in=4,looseness=2.5] (m);
      \end{scope}
    \end{tikzpicture}
  \end{center}
  \vspace{-.5em}
  \pause
  
  Idea: consider only strongly connected components
  $\SN(\{1\}_{\mit{top}}/R)$, 
  $\SN(\{3\}_{\mit{top}}/R)$.
  \end{example}
\end{frame}

\section{Subterm Criterion}
\themex{Subterm Criterion}