\begin{frame}[t]
  \small
  
  \begin{example}
  \smallskip
  \begin{itemize}
  \item
  rewrite rules
  \[
  \GREEN{\begin{array}[t]{r@{~}c@{~}l@{\qquad}r@{~}c@{~}%
  l@{\qquad}c@{\qquad}r@{~}c@{~}l}
  0+0 & \to & 0 & 1+0 & \to & 1 & \cdots & 9+0 & \to & 9 \\
  0+1 & \to & 1 & 1+1 & \to & 2 & \cdots & 9+1 & \to & 1:0 \\
  0+2 & \to & 2 & 1+2 & \to & 3 & \cdots & 9+2 & \to & 1:1 \\
  0+3 & \to & 3 & 1+3 & \to & 4 & \cdots & 9+3 & \to & 1:2 \\
  0+4 & \to & 4 & 1+4 & \to & 5 & \cdots & 9+4 & \to & 1:3 \\
  0+5 & \to & 5 & 1+5 & \to & 6 & \cdots & 9+5 & \to & 1:4 \\
  0+6 & \to & 6 & 1+6 & \to & 7 & \cdots & 9+6 & \to & 1:5 \\
  0+7 & \to & 7 & 1+7 & \to & 8 & \cdots & 9+7 & \to & 1:6 \\
  0+8 & \to & 8 & 1+8 & \to & 9 & \cdots & 9+8 & \to & 1:7 \\
  0+9 & \to & 9 & 1+9 & \to & 1:0 & \cdots & 9+9 & \to & 1:8 \\
  \multicolumn{7}{@{}l}{
  \begin{array}{@{}r@{~}c@{~}l}
  x + (y : z) & \to & y : (x + z)
  \end{array}} &
  0 : x & \to & x \\
  \multicolumn{7}{@{}l}{
  \begin{array}{@{}r@{~}c@{~}l}
  (x : y) + z & \to & x : (y + z)
  \end{array}} &
  \makebox[0cm][r]{$x : (y : z)$} & \to & (x + y) : z \\
  \end{array}}
  \]
  \item
  term
  \smallskip
  \[
  \GREEN{((0 : (1 + 2)) + (3 + 4)) + (5 + 6)}
  \]
  \end{itemize}
  \end{example}
\end{frame}