\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}