# bussproofs

The bussproofs extension implements the `bussproofs` style package from LaTeX. See the CTAN page for more information and documentation of bussproofs.

Note that there are a couple of important differences between the use of the package in MathJax compared to actual LaTeX. First, proofs always have to be in a prooftree environment, i.e., inference macros are only recognised if they are enclosed in `\begin{prooftree}` and `\end{prooftree}`. Consequently the `\DisplayProof` command is not necessary.

Second, unlike in the LaTeX package, options for abbreviated inference rule macros do not have to be manually set. All abbreviated macros are directly available. Thus commands like `\BinaryInfC` and `\BIC` can be used immediately and interchangeably.

For example:

    \begin{prooftree}
    \AxiomC{}
    \RightLabel{Hyp$^{1}$}
    \UnaryInfC{$P$}
    \AXC{$P\to Q$}
    \RL{$\to_E$}
    \BIC{$Q^2$}
    \AXC{$Q\to R$}
    \RL{$\to_E$}
    \BIC{$R$}
    \AXC{$Q$}
    \RL{Rit$^2$}
    \UIC{$Q$}
    \RL{$\wedge_I$}
    \BIC{$Q\wedge R$}
    \RL{$\to_I$$^1$}
    \UIC{$P\to Q\wedge R$}
    \end{prooftree}

Also note that the bussproofs commands for sequent calculus derivations are not yet fully implemented.

This extension is loaded automatically when the autoload extension is used. To load the bussproofs extension explicitly, add `'[tex]/bussproofs'` to the `load` array of the `loader` block of your MathJax configuration, and add `'bussproofs'` to the `packages` array of the `tex` block.

    window.MathJax = {
      loader: {load: ['[tex]/bussproofs']},
      tex: {packages: {'[+]': ['bussproofs']}}
    };

Alternatively, use `\require{bussproofs}` in a TeX expression to load it dynamically from within the math on the page, if the require extension is loaded.

## bussproofs Commands

The bussproofs extension implements the following macros: `\alwaysDashedLine`, `\alwaysNoLine`, `\alwaysRootAtBottom`, `\alwaysRootAtTop`, `\alwaysSingleLine`, `\alwaysSolidLine`, `\AXC`, `\Axiom`, `\AxiomC`, `\BIC`, `\BinaryInf`, `\BinaryInfC`, `\dashedLine`, `\fCenter`, `\LeftLabel`, `\LL`, `\noLine`, `\QuaternaryInf`, `\QuaternaryInfC`, `\QuinaryInf`, `\QuinaryInfC`, `\RightLabel`, `\RL`, `\rootAtBottom`, `\rootAtTop`, `\singleLine`, `\solidLine`, `\TIC`, `\TrinaryInf`, `\TrinaryInfC`, `\UIC`, `\UnaryInf`, `\UnaryInfC`

And the following environments: `prooftree`