\begin{frame} \small \begin{theorem} For orthogonal TRSs, every fair strategy is cofinal. \end{theorem} \pause \begin{proof} Let $\rho : t_0 \to t_1 \to \ldots$ be a fair rewrite sequence. \medskip\pause Let $\tau : t_0 \to u_0$. We show that $u_0 \to^* t_n$ for some $t_n$ in $\rho$. \pause \begin{center} \begin{tikzpicture}[thick,node distance=20mm] \node (s1) {$u_0$}; \node [right of=s1] (s2) {$u_1$}; \node [right of=s2] (s3) {$u_2$}; \node [right of=s3] (sd) {$\ldots$}; \node [right of=sd] (sn) {$u_n$}; \node [above of=s1,node distance=10mm] (t1) {$t_0$}; \node [right of=t1] (t2) {$t_1$}; \node [right of=t2] (t3) {$t_2$}; \node [right of=t3] (td) {$\ldots$}; \node [right of=td] (tn) {$t_n$}; \node [right of=tn] (ti) {$\ldots$}; \begin{scope}[->] \draw (t1) -- (t2); \draw (t2) -- (t3); \draw (t3) -- (td); \draw (td) -- (tn); \draw (tn) -- (ti); \draw (t1) -- (s1) node [midway,right] {$\tau$}; \end{scope} \begin{scope}[->>] \draw (s1) -- (s2); \draw (s2) -- (s3); \draw (s3) -- (sd); \draw (sd) -- (sn); \draw (t2) -- (s2) node [midway,right] {$\tau\project\rho_1$}; \draw (t3) -- (s3) node [midway,right] {$\tau\project\rho_2$}; \end{scope} \draw (tn) -- (sn) node [midway,right] {$\varnothing$}; \end{tikzpicture} \end{center} \vspace{-2ex} Here $\rho_i$ consists of the first $i$ steps of $\rho$. \medskip\pause By fairness of $\rho$ there exists $n$ such that $\tau \project \rho_n = \varnothing$. \pause Hence $u_n = t_n$ and $u_0 \to^* t_n$. \medskip\pause The reduction $u_0 \to u_1 \to \ldots \to u_n \to t_{n+1} \to t_{n+2}$ is fair again.\\ (every redex occurrence in $t_n$ is eventually secured) \medskip\pause By induction over the length of $t_0 \to^* u_0$ we get $u_0 \to^* t_n$ for some $t_n$ in $\rho$. \end{proof} \end{frame}