\begin{frame}[t] \small \begin{definition} \alert{Leftmost innermost} strategy always reduces the leftmost of the innermost redexes. \end{definition} \pause \begin{example}[cont'd] \vspace{-1.5ex} \GREEN{ \begin{align*} (0:\highlight{(1+2)})+(3+4)+(5+6) &\onslide<3->{\to (\highlight{(0:3)}+(3+4))+(5+6)}\\ &\onslide<4->{\to (3+\highlight{(3+4)})+(5+6)} \\ &\onslide<5->{\to \highlight{(3+7)}+(5+6)}\\ &\onslide<6->{\to (1:0)+\highlight{(5+6)}}\\ &\onslide<7->{\to \highlight{(1:0)+(1:1)}} \\ &\onslide<8->{\to 1:\highlight{(0+(1:1))}}\\ &\onslide<9->{\to 1:(1:\highlight{(0+1)})}\\ &\onslide<10->{\to \highlight{1:(1:1)}} \\ &\onslide<11->{\to \highlight{(1+1)}:1}\\ &\onslide<12->{\to 2:1} \end{align*} } \vspace{-3ex} \end{example} \end{frame}