계정: 로그인
AA 📝
시연용 공개 문서

Bussproofs, xcolor 예제

결과


        \begin{prooftree}
                \AXC{}\RL{\small Ax}
                \UIC{$\alert{f:}\varphi\land\psi\to\sigma\vdash\alert{f:}\varphi\land\psi\to\sigma$}
                \AXC{}\RL{\small Ax}
                \UIC{$\alert{x:}\varphi\vdash\alert{x:}\varphi$}
                \AXC{}\RL{\small Ax}
                \UIC{$\alert{y:}\psi\vdash\alert{y:}\psi$}
                \RL{\small $\land$-I}\BIC{$\alert{x:}\varphi,\alert{y:}\psi\vdash%
                        \alert{\langle x,y\rangle :}\varphi\land\psi$}
                \RL{\small $\to$-E}\BIC{$\alert{f:}\varphi\land\psi\to\sigma,\alert{x:}\varphi,\alert{y:}\psi\vdash %
                        \alert{f\ \langle x,y\rangle :}\sigma$}
                \RL{\small $\to$-I}\UIC{$\alert{f:}\varphi\land\psi\to\sigma,\alert{x:}\varphi\vdash %
                        \alert{\lambda y^\psi.f\ \langle x,y\rangle :}\psi\to\sigma$}
                \RL{\small $\to$-I}\UIC{$\alert{f:}\varphi\land\psi\to\sigma\vdash %
                        \alert{\lambda x^\varphi.\lambda y^\psi.f\ \langle x,y\rangle :}\varphi\to\psi\to\sigma$}
                \RL{\small $\to$-I}\UIC{$\vdash %
                        \alert{\lambda f^{\varphi\land\psi\to\sigma}.%
                        \lambda x^\varphi.\lambda y^\psi.f\ \langle x,y\rangle :}%
                        (\varphi\land\psi\to\sigma)\to\varphi\to\psi\to\sigma$}
        \end{prooftree}

위키 문서 내용 (코드)

   1 {{{#!latex
   2 \usepackage{bussproofs,xcolor}
   3 \EnableBpAbbreviations
   4 \newcommand{\alert}[1]{\textcolor{red}{#1}}
   5 %%end-prologue%%
   6         \begin{prooftree}
   7                 \AXC{}\RL{\small Ax}
   8                 \UIC{$\alert{f:}\varphi\land\psi\to\sigma\vdash\alert{f:}\varphi\land\psi\to\sigma$}
   9                 \AXC{}\RL{\small Ax}
  10                 \UIC{$\alert{x:}\varphi\vdash\alert{x:}\varphi$}
  11                 \AXC{}\RL{\small Ax}
  12                 \UIC{$\alert{y:}\psi\vdash\alert{y:}\psi$}
  13                 \RL{\small $\land$-I}\BIC{$\alert{x:}\varphi,\alert{y:}\psi\vdash%
  14                         \alert{\langle x,y\rangle :}\varphi\land\psi$}
  15                 \RL{\small $\to$-E}\BIC{$\alert{f:}\varphi\land\psi\to\sigma,\alert{x:}\varphi,\alert{y:}\psi\vdash %
  16                         \alert{f\ \langle x,y\rangle :}\sigma$}
  17                 \RL{\small $\to$-I}\UIC{$\alert{f:}\varphi\land\psi\to\sigma,\alert{x:}\varphi\vdash %
  18                         \alert{\lambda y^\psi.f\ \langle x,y\rangle :}\psi\to\sigma$}
  19                 \RL{\small $\to$-I}\UIC{$\alert{f:}\varphi\land\psi\to\sigma\vdash %
  20                         \alert{\lambda x^\varphi.\lambda y^\psi.f\ \langle x,y\rangle :}\varphi\to\psi\to\sigma$}
  21                 \RL{\small $\to$-I}\UIC{$\vdash %
  22                         \alert{\lambda f^{\varphi\land\psi\to\sigma}.%
  23                         \lambda x^\varphi.\lambda y^\psi.f\ \langle x,y\rangle :}%
  24                         (\varphi\land\psi\to\sigma)\to\varphi\to\psi\to\sigma$}
  25         \end{prooftree}
  26 }}}