thm__church_rosser_theorem.tex

\documentclass{classes/tikzcd}

\begin{document}
  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
              & L                       &                 \\
    N \ar[ur] &                         & K \ar[ul, swap] \\
              & M \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
              & P                                   &                         \\
    C \ar[ur] &                                     & \qabs x F \ar[ul, swap] \\
              & A = \qabs x E \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
              & R                       &                 \\
    D \ar[ur] &                         & G \ar[ul, swap] \\
              & B \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                                & P \aequiv \qabs x Q                 &                         \\
    C \aequiv \qabs x H \ar[ur] &                                     & \qabs x F \ar[ul, swap] \\
                                & A = \qabs x E \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                           & L                                          &                 \\
    N = \qabs x Lx \ar[ur] &                                            & K \ar[ul, swap] \\
                           & M \aequiv \qabs x Kx \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                                     & L = P[x \mapsto Q]                      &                                      \\
    N = C[x \mapsto D] \ar[ur, swap] &                                         & K = (\qabs x H)F \ar[ul, swap, swap] \\
                                     & M = (\qabs x A) B \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                         & L = PQ                                          &                            \\
    N \aequiv PD \ar[ur] &                                                 & K = EF \ar[ul, swap, swap] \\
                         & M \aequiv (\qabs x E x) B \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                                     & L = R[y \mapsto Q]                                        &                                      \\
    N \aequiv R[y \mapsto D] \ar[ur] &                                                           & K \aequiv (\qabs y P)F \ar[ul, swap] \\
                                     & M \aequiv (\qabs x (\qabs y P) x) B \ar[ul] \ar[ur, swap] &
  \end{tikzcd}

  \begin{tikzcd}[every arrow/.append style={"{\overset {\Anon} {\parallel}}" marking}]
                                     & L = P[x \mapsto Q]                      &                                        \\
    N = C[x \mapsto D] \ar[ur, swap] &                                         & K \aequiv E[x \mapsto F] \ar[ul, swap] \\
                                     & M = (\qabs x A) B \ar[ul] \ar[ur, swap] &
  \end{tikzcd}
\end{document}