\begin{frame}
  \frametitle{Compression and Parallel Moves}
  
  \begin{theorem}[Compression]
  Let $\atrs$ be an left-linear TRS.
  Then $s \ired t$ implies $s \to^{\le \omega} t$.
  \end{theorem}
  That is, every strongly convergent reduction can be compressed to length $\le \omega$.
  \pause\bigskip
  
  \begin{theorem}[Parallel Moves]
  Let $\atrs$ be an orthogonal TRS.
  Then $t_1 \mathrel{\reflectbox{$\parr$}} s \ired t_2 \;\Rightarrow\; t_1 \ired \cdot \mathrel{\reflectbox{$\parr$}} t_2$.
  \begin{center}
  \begin{tikzpicture}[node distance=15mm]
    \node (s) {$s$};
    \node (t1) [below of=s] {$t_1$};
    \node (t2) [right of=s,node distance=50mm] {$t_2$};
    \node (s') [below of=t2] {$s'$};
    
    \draw [infred] (s) -- (t2);
    \draw [infred] (t1) -- (s');
    \draw [infred] (s) -- (t1);
    \draw [infred] (t2) -- (s');
    
    \draw ($(s)!.5!(t1) + (-2mm,1mm)$) -- ($(s)!.5!(t1) + (2mm,1mm)$);
    \draw ($(s)!.5!(t1) + (-2mm,2mm)$) -- ($(s)!.5!(t1) + (2mm,2mm)$);
    \draw ($(t2)!.5!(s') + (-2mm,1mm)$) -- ($(t2)!.5!(s') + (2mm,1mm)$);
    \draw ($(t2)!.5!(s') + (-2mm,2mm)$) -- ($(t2)!.5!(s') + (2mm,2mm)$);
  \end{tikzpicture}
  \end{center}
  \end{theorem}
\end{frame}