ex__natural_number_arithmetic_grammar__derivation.tex

\documentclass{classes/tikzcd}

\begin{document}
  \begin{tikzcd}[column sep=small, every arrow/.append style={Rightarrow}]
    E \ar[r]                                             & (E \syntimes E) \ar[r]                                  & (N \syntimes E) \ar[r]                            & (\syn1 B \syntimes E) \ar[r]                  & (\syn1 \syn0 \syntimes E) \ar[d]              \\
    (\syn1 \syn0 \syntimes (\syn1 \synplus \syn1 \syn0)) & (\syn1 \syn0 \syntimes (\syn1 \synplus \syn1 B)) \ar[l] & (\syn1 \syn0 \syntimes (\syn1 \synplus E)) \ar[l] & (\syn1 \syn0 \syntimes (N \synplus E)) \ar[l] & (\syn1 \syn0 \syntimes (E \synplus E)) \ar[l]
  \end{tikzcd}

  \begin{tikzcd}[column sep=tiny, row sep=tiny, every arrow/.append style={Rightarrow}]
                      & E \synplus E \ar[r]  & E \syntimes E \synplus E \ar[r] & N \syntimes E \synplus E \ar[r] & \syn1 B \syntimes E \synplus E \ar[dr] &                                           &               &                                                  \\
    E \ar[ur] \ar[dr] &                      &                                 &                                 &                                        & \syn1 \syn0 \syntimes E \synplus E \ar[r] & \cdots \ar[r] & \syn1 \syn0 \syntimes \syn1 \synplus \syn1 \syn0 \\
                      & E \syntimes E \ar[r] & N \syntimes E \ar[r]            & \syn1 B \syntimes E \ar[r]      & \syn1 \syn0 \syntimes E \ar[ur]        &                                           &               &
  \end{tikzcd}
\end{document}