\begin{frame} \small \vspace{-1ex} \begin{theorem} \smallskip For orthogonal TRSs \begin{itemize} \item \structure{full substitution} and \structure{parallel outermost} strategies are \alert{normalizing} \vspace{-.5ex} \item<2-> \structure{innermost} strategies are \alert{perpetual} \vspace{-.5ex} \item<3-> \structure{leftmost outermost} strategy is \alert{not normalizing} \vspace{-.5ex} \item<4-> \structure{full substitution} is \alert{fair} \end{itemize} \smallskip \end{theorem} \begin{example}<4-> \vspace{-2ex} \GREEN{\begin{xalignat*}{3} \m{a} &\to \m{b} & \m{c} &\to \m{c} & \m{f}(x,\m{b}) &\to \m{b} \end{xalignat*}} \vspace{-4.5ex} \begin{itemize} \item \makebox[35mm][l]{\structure{leftmost outermost}} \GREEN{\( \m{f}(\alert<5->{\m{c}},\m{a}) \onslide<5->{\to \m{f}(\alert<6->{\m{c}},\m{a})} \onslide<6->{\to \m{f}(\alert<7->{\m{c}},\m{a})} \onslide<7->{\to \cdots} \)} \item \makebox[35mm][l]{\structure{leftmost innermost}} \GREEN{\( \m{f}(\alert<8->{\m{c}},\m{a}) \onslide<8->{\to \m{f}(\alert<9->{\m{c}},\m{a})} \onslide<9->{\to \m{f}(\alert<10->{\m{c}},\m{a})} \onslide<10->{\to \cdots} \)} \item \makebox[35mm][l]{\structure{parallel outermost}} \GREEN{\( \m{f}(\alert<11->{\m{c}},\alert<11->{\m{a}}) \onslide<11->{\parr \alert<12->{\m{f}}(\m{c},\m{b})} \onslide<12->{\to \m{b}} \)} \item \makebox[35mm][l]{\structure{parallel innermost}} \GREEN{\( \m{f}(\alert<13>{\m{c}},\alert<13->{\m{a}}) \onslide<13->{\parr \m{f}(\alert<14->{\m{c}},\m{b})} \onslide<14->{\to \m{f}(\alert<15->{\m{c}},\m{b})} \onslide<15->{\to \cdots} \)} \item \makebox[35mm][l]{\structure{full substitution}} \GREEN{\( \m{f}(\alert<16->{\m{c}},\alert<16->{\m{a}}) \onslide<16->{\dev \alert<17->{\m{f}}(\alert<17->{\m{c}},\m{b})} \onslide<17->{\dev \m{b}} \)} \end{itemize} \end{example} \end{frame}