summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/bussproofs
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/bussproofs
Initial commit
Diffstat (limited to 'macros/latex/contrib/bussproofs')
-rw-r--r--macros/latex/contrib/bussproofs/BussGuide2.pdfbin0 -> 75218 bytes
-rw-r--r--macros/latex/contrib/bussproofs/BussGuide2.tex775
l---------macros/latex/contrib/bussproofs/README1
-rw-r--r--macros/latex/contrib/bussproofs/README.txt31
-rw-r--r--macros/latex/contrib/bussproofs/bussproofs.sty1137
-rw-r--r--macros/latex/contrib/bussproofs/testbp2.pdfbin0 -> 43839 bytes
-rw-r--r--macros/latex/contrib/bussproofs/testbp2.tex321
7 files changed, 2265 insertions, 0 deletions
diff --git a/macros/latex/contrib/bussproofs/BussGuide2.pdf b/macros/latex/contrib/bussproofs/BussGuide2.pdf
new file mode 100644
index 0000000000..84b9556c8a
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/BussGuide2.pdf
Binary files differ
diff --git a/macros/latex/contrib/bussproofs/BussGuide2.tex b/macros/latex/contrib/bussproofs/BussGuide2.tex
new file mode 100644
index 0000000000..35bb699f4b
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/BussGuide2.tex
@@ -0,0 +1,775 @@
+%
+%Documentation by Peter Smith, July 2004, March 2012
+%
+%comments to peter_smith@me.com
+%
+
+\documentclass[11pt]{article}
+\usepackage{graphicx}
+\usepackage{amssymb}
+%\usepackage{epstopdf}
+
+\usepackage{bussproofs}
+\def\fCenter{{\mbox{$\vdash$}}}
+
+\DeclareGraphicsRule{.tif}{png}{.png}{`convert #1 `basename #1 .tif`.png}
+
+\textwidth = 6.5 in
+\textheight = 9 in
+\oddsidemargin = 0.0 in
+\evensidemargin = 0.0 in
+\topmargin = 0.0 in
+\headheight = 0.0 in
+\headsep = 0.0 in
+\parskip = 0.0in
+\parindent = 0.2in
+
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{definition}{Definition}
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%
+%%%
+%%% front matter
+%%%
+%%%%%%%%%%%%%%%%%%
+
+\thispagestyle{empty}
+\begin{center}
+ \Huge{\LaTeX\ for Logicians}\\[16pt]
+ \huge{\texttt{bussproofs.sty}}\\[8pt]
+ \huge{A User Guide}\\[16pt]
+\end{center}
+\vspace{0.5in}
+\tableofcontents
+\vspace{0.3in}
+\begin{center}
+ \fbox{\parbox{4.5in}{\begin{center}The latest version of \texttt{bussproofs.sty}
+ is 1.1, July 2011.\end{center}}}
+\end{center}
+\vspace{0.4in}
+\begin{center}
+ \small{Guide version 1.1 March 2012. Corrections/suggestions to
+ \texttt{peter}\_$\!$\_\texttt{smith@me.com}}
+ \\
+ \small{\LaTeX\ for Logicians is at \texttt{http://www.logicmatters.net}}
+\end{center}
+\newpage
+
+%%%%%%%%%%%%%%%%%%
+%%%
+%%% main matter
+%%%
+%%%%%%%%%%%%%%%%%%
+\section{Introduction}
+
+\noindent Sam Buss's powerful and flexible package {\texttt{bussproofs.sty}} offers macros for setting natural deduction and sequent proofs in two different styles. The key difference between the two styles is illustrated by the difference between
+\begin{prooftree}
+\AxiomC{$\Gamma, A, B \vdash C$}
+\UnaryInfC{$\Gamma, A \vdash (B \to C)$}
+\UnaryInfC{$\Gamma \vdash (A \to (B \to C))$}
+\end{prooftree}
+and
+\begin{prooftree}
+\Axiom$\Gamma, A, B\ \fCenter\ C$
+\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
+\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
+\end{prooftree}
+In one style, the sequents above and below the inference line are centered; in the other, the sequents are placed so as to align their deducibility signs.
+
+We can divide {\texttt{bussproofs.sty}}'s commands for building proofs into four types:
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item \emph{the structural commands} for producing proof trees in the \emph{centering} style;
+\item \emph{more structural commands} for producing proof trees in the \emph{sequent-aligning} style;
+\item \emph{additional commands} for adding labels, and changing the setting of inference lines (selecting double, dashed lines, etc.);
+\item \emph{fine-tuning commands} for adjusting the spacing and layout of the proof.
+\end{itemize}
+{\texttt{bussproofs.sty}} also provides an additional command which enables some very laconic shorthand for the most commonly used commands. We describe these in Section~\ref{abbrev}; but we avoid using shorthand until the full commands have been explained and made familiar.
+
+
+
+\section{`Centered' proofs: the structural commands}
+\subsection{The commands} There are four basic proof-building commands for producing proofs in the centered style:
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\AxiomC{=\textit{form}\verb=}=
+\item \verb=\UnaryInfC{=\textit{form}\verb=}=
+\item \verb=\BinaryInfC{=\textit{form}\verb=}=
+\item \verb=\TrinaryInfC{=\textit{form}\verb=}=
+\end{description}
+\end{quote}
+where `\textit{form}' holds the place for a formula or sequent. Note
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item The use of the surrounding `\verb={}='s is mandatory.
+\item By default, \textit{form} is set in text mode: if you want to set some or all of \textit{form} in math mode, then you need to use \verb=$='s in the usual way.
+\end{itemize}
+Chaining a series of those commands, however, is not enough to cause a proof to be set. To display a proof you must use one of
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\DisplayProof=, a command placed at the end of a list of proof-building commands, which produces an in-line proof at the current insertion point.
+\item \verb=\begin{prooftree} ... \end{prooftree}=, an environment which contains a list of proof-building commands, and which produces a proof in a centered display.
+\end{description}
+\end{quote}
+Again, note
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item The \verb=\DisplayProof= command allows you to put proofs anywhere normal text might appear; for example, in a paragraph, in a table, in a tabbing environment, etc.
+\item To generate a proof in a centered display, do \emph{not} use \verb=$$ ... $$= or \verb=\[ ... \]=.
+\end{itemize}
+
+\subsection{Usage} It will be a \emph{lot} clearer if we start with examples rather than begin with an abstract description of the principles for chaining proof-building commands! So here goes \ldots
+\begin{quote}
+\begin{verbatim}
+\AxiomC{A}
+\UnaryInfC{D}
+\DisplayProof
+\end{verbatim}
+\end{quote}
+produces the one-step proof
+\AxiomC{A}
+\UnaryInfC{D}
+\DisplayProof
+in the current line. While
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\AxiomC{A}
+\AxiomC{B}
+\BinaryInfC{D}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+displays the proof
+\begin{prooftree}
+\AxiomC{A}
+\AxiomC{B}
+\BinaryInfC{D}
+\end{prooftree}
+centered and set off from the surrounding text. So it will be no surprise to learn that
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\AxiomC{A}
+\AxiomC{B}
+\AxiomC{C}
+\TrinaryInfC{D}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+produces the proof
+\begin{prooftree}
+\AxiomC{A}
+\AxiomC{B}
+\AxiomC{C}
+\TrinaryInfC{D}
+\end{prooftree}
+Two comments:
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item You'll get an error message if there's a mismatch between the arity of the \verb=\...aryInfC= command and the number of inputs.
+\item \texttt{bussproof.sty} does not allow arbitrary numbers of premisses appearing as separate \textit{form} items above the inference line.
+\end{itemize}
+
+So much for one-step proofs. Now things get a little more fun \ldots.
+Consider
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{A}
+ \AxiomC{B}
+ \AxiomC{C}
+ \BinaryInfC{D}
+ \BinaryInfC{E}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+This produces the proof
+\begin{quote}
+\begin{prooftree}
+\AxiomC{A}
+\AxiomC{B}
+\AxiomC{C}
+\BinaryInfC{D}
+\BinaryInfC{E}
+\end{prooftree}
+\end{quote}
+Why? Think of the first \verb=\BinaryInfC= command as `using up' as premisses the two axioms immediately above it. Then the second \verb=\BinaryInfC= command takes as premisses `D' immediately above it and then searches up to the next `unused' item, i.e. `A'. The inputs to a particular \verb=\BinaryInfC= command are then set right-to-left in the order in which the {command} finds them as it looks {up} the series of commands. Which means, as we want, that {the inputs to a particular inference are set left-to-right in the same order as they occur in the chain of commands}.
+
+It probably helps if we set out the proof-building commands like this:
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{A}
+ \AxiomC{B}
+ \AxiomC{C}
+ \BinaryInfC{D}
+ \BinaryInfC{E}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+That pretty much replicates the layout of the tree we want. This indeed is one of the \emph{very} nice features of \texttt{bussproofs.sty} -- the instructions to build a proof-tree can be set out to look very like the proof we want.
+
+Suppose then that we want to set a tree that is arranged like this:
+\begin{prooftree}
+\AxiomC{A}
+\UnaryInfC{B}
+\AxiomC{C}
+\BinaryInfC{D}
+\AxiomC{E}
+\AxiomC{F}
+\BinaryInfC{G}
+\UnaryInfC{H}
+\BinaryInfC{J}
+\end{prooftree}
+The following does the trick:
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{A}
+ \UnaryInfC{B}
+ \AxiomC{C}
+ \BinaryInfC{D}
+ \AxiomC{E}
+ \AxiomC{F}
+ \BinaryInfC{G}
+ \UnaryInfC{H}
+ \BinaryInfC{J}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+In sum, then, the rule to produce a given tree is
+\begin{quote}
+\emph{Set out the commands for the left-hand sub-proof first; and then within a sub-proof, do its left-hand sub-sub-proof first; and so on.}
+\end{quote}
+Two more points about general structure:
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item The command \verb=\noLine= can be inserted before any inference command to suppress the drawing of an inference line.
+\item Null axioms are allowed!
+\end{itemize}
+Hence, the commands
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{$A \lor B$}
+ \AxiomC{[$A$]}
+ \noLine
+ \UnaryInfC{$C$}
+ \AxiomC{[$B$]}
+ \noLine
+ \UnaryInfC{$C$}
+ \TrinaryInfC{$C$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+yield
+\begin{prooftree}
+\AxiomC{$A \lor B$}
+\AxiomC{[$A$]}
+\noLine
+\UnaryInfC{$C$}
+\AxiomC{[$B$]}
+\noLine
+\UnaryInfC{$C$}
+\TrinaryInfC{$C$}
+\end{prooftree}
+And we can use the fact that null axioms are allowed to generate natural deduction proofs with formulae overlined to indicate the discharge of premisses (by treating the formula to be overlined as a unary inference from a null axiom). For example:
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{$P$}
+ \AxiomC{}
+ \UnaryInfC{$\neg P$}
+ \BinaryInfC{$\bot$}
+ \UnaryInfC{$\neg\neg P$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+generates the proof
+\begin{prooftree}
+ \AxiomC{$P$}
+ \AxiomC{}
+ \UnaryInfC{$\neg P$}
+ \BinaryInfC{$\bot$}
+ \UnaryInfC{$\neg\neg P$}
+\end{prooftree}
+
+\subsection{More than three premisses}
+
+So far we've only considered inference steps that take one premiss (like double negation), two premisses (like modus ponens), or three inputs (like or-elimination). But Buss proofs in fact supplies -- should you want it -- the capacity to deal with four or five premisses. The syntax is as you would expect. We have the two commands
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\QuaternaryInfC{=\textit{form}\verb=}=
+\item \verb=\QuinaryInfC{=\textit{form}\verb=}=
+\end{description}
+\end{quote}
+These aren't pointless! After all, you might want to illustrate the $\omega$-rule thus:
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\AxiomC{$\varphi(0)$}
+\AxiomC{$\varphi(1)$}
+\AxiomC{$\varphi(2)$}
+\AxiomC{$\varphi(3)$}
+\AxiomC{$\ldots$}
+\QuinaryInfC{$\forall n\varphi(n)$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+to give
+\begin{quote}
+\begin{prooftree}
+\AxiomC{$\varphi(0)$}
+\AxiomC{$\varphi(1)$}
+\AxiomC{$\varphi(2)$}
+\AxiomC{$\varphi(3)$}
+\AxiomC{$\ldots$}
+\QuinaryInfC{$\forall n\varphi(n)$}
+\end{prooftree}
+\end{quote}
+
+
+
+
+\section{`Sequent-aligned' proofs: the structural commands}
+\subsection{The commands} There are four basic proof-building commands for producing proofs in the second style:
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\Axiom$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
+\item \verb=\UnaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
+\item \verb=\BinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
+\item \verb=\TrinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
+\end{description}
+\end{quote}
+where `\textit{form}' holds the place for a formula or formulae, and \verb=\fCenter= marks the point of alignment.
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item This time, the use of the surrounding `\verb=$='s is mandatory; and material between the `\verb=$='s is set in math mode.
+\item The `\verb=\fCenter=' is by default just a place-marker; however, it can be redefined to be printed character such as a sequent arrow or turnstile.
+\end{itemize}
+And for multi-premiss usage, we also have the additional commands:
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\QuaternaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=
+\item \verb=\QuinaryInf$= \textit{form} \verb=\fCenter= \textit{form} \verb=$=\end{description}
+\end{quote}
+
+\subsection{Usage}
+The basic usage is illustrated by the following:
+\def\fCenter{}
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\Axiom$A, B, C, D,\fCenter\ E, F$
+\UnaryInf$A, B,\fCenter\ C, D, E, F$
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+\begin{prooftree}
+\Axiom$A, B, C, D,\fCenter\ E, F$
+\UnaryInf$A, B,\fCenter\ C, D, E, F$
+\end{prooftree}
+Now let's redefine \verb=\fCenter= to be the turnstile surrounded by spaces. Then
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\def\fCenter{\ \vdash\ }
+\Axiom$A, B, C, D \fCenter E, F$
+\UnaryInf$A, B \fCenter C, D, E, F$
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+produces
+\begin{prooftree}
+\def\fCenter{\ \vdash\ }
+\Axiom$A, B, C, D \fCenter E, F$
+\UnaryInf$A, B \fCenter C, D, E, F$
+\end{prooftree}
+However, it is in general preferable to redefine \verb=\fCenter= using an \verb=\mbox= as in the next example (this allows more options):
+\begin{quote}
+\begin{verbatim}
+\def\fCenter{\mbox{\Large$\rightarrow$}}
+\begin{prooftree}
+\Axiom$\Gamma, A, B\ \fCenter\ B$
+\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
+\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+produces
+\def\fCenter{\mbox{\Large$\rightarrow$}}
+\begin{prooftree}
+\Axiom$\Gamma, A, B\ \fCenter\ B$
+\UnaryInf$\Gamma, A\ \fCenter\ (B \to C)$
+\UnaryInf$\Gamma\ \fCenter\ (A \to (B \to C))$
+\end{prooftree}
+And this time, since the \verb=\def\fCenter{...}= command precedes the following \verb=prooftree= environment, it will stay in effect until overridden later in the document.
+\begin{itemize}
+\item The chaining of multiple sequent-aligning commands to build complex proofs works just as with the earlier centering-style commands.
+\item It should go without saying that the point of the \verb=\BinaryInf$...$= command is not to align the sequent turnstile, (arrow, or whatever) in the conclusion of the two-premiss inference with the turnstiles in the premisses, but to provide a new alignment point for later sequents.
+\item Mixing and matching sensible combinations of \verb=C{...}=-type centering commands and \verb=$...$=-type sequent-aligning commands is in fact legitimate.
+\end{itemize}
+Thus, to illustrate the last point,
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+\def\fCenter{\mbox{\ $\vdash$\ }}
+\AxiomC{$\Gamma \vdash A$}
+\AxiomC{$A, B \vdash C$}
+\BinaryInf$\Gamma, B \fCenter C$
+\UnaryInf$\Gamma \fCenter B \to C$
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+is acceptable, and yields
+\begin{prooftree}
+\def\fCenter{\mbox{\ $\vdash$\ }}
+\AxiomC{$\Gamma \vdash A$}
+\AxiomC{$A, B \vdash C$}
+\BinaryInf$\Gamma, B \fCenter C$
+\UnaryInf$\Gamma \fCenter B \to C$
+\end{prooftree}
+
+
+
+\section{Additional layout commands}
+Conventionally, the proof
+\begin{prooftree}
+ \AxiomC{$P$}
+ \AxiomC{}
+ \UnaryInfC{$\neg P$}
+ \BinaryInfC{$\bot$}
+ \UnaryInfC{$\neg\neg P$}
+\end{prooftree}
+needs labelling. This section describes how to add labels to proofs, and also how to change the style of inference-line (to double lines, etc.).
+
+\subsection{Adding labels} There are two commands for decorating a proof with labels:
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\LeftLabel{text}=
+\item \verb=\RightLabel{text}=
+ \end{description}
+\end{quote}
+These put \verb=text= as a label to the left/right of the next inference line (and they work even if \verb=\noLine= is used and line isn't actually drawn).
+
+So, for example, the commands
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{$\Gamma, A \vdash B$}
+ \LeftLabel{Conditional Proof:}
+ \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+will generate
+\begin{prooftree}
+ \AxiomC{$\Gamma, A \vdash B$}
+ \LeftLabel{Conditional Proof:}
+ \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
+\end{prooftree}
+You can insert spacing commands and other text commands into the label text, so e.g. substituting \verb=\LeftLabel{Conditional Proof:\quad}= will generate
+\begin{prooftree}
+ \AxiomC{$\Gamma, A \vdash B$}
+ \LeftLabel{Conditional Proof:\quad}
+ \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
+\end{prooftree}
+However, there is also a global command for adjusting the position of labels, and in general it might be better to use that.
+
+You can reduce the size of the label font, so that
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{$P$}
+ \AxiomC{}
+ \RightLabel{\scriptsize(1)}
+ \UnaryInfC{$\neg P$}
+ \BinaryInfC{$\bot$}
+ \RightLabel{\scriptsize(1)}
+ \UnaryInfC{$\neg\neg P$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+will set the conventionally annotated proof
+\begin{prooftree}
+ \AxiomC{$P$}
+ \AxiomC{}
+ \RightLabel{\scriptsize(1)}
+ \UnaryInfC{$\neg P$}
+ \BinaryInfC{$\bot$}
+ \RightLabel{\scriptsize(1)}
+ \UnaryInfC{$\neg\neg P$}
+\end{prooftree}
+\subsection{Varieties of inference lines} The inference line between premiss and derived conclusion defaults, as we've seen, to a single solid line. But this can be changed, either locally or more globally. The local change commands are
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\noLine=
+\item \verb=\singleLine=
+\item \verb=\doubleLine=
+\item \verb=\solidLine=
+\item \verb=\dottedLine=
+\item \verb=\dashedLine=
+\end{description}
+\end{quote}
+Each applies to the next inference, and line-\emph{number} and line-\emph{type} commands can be combined: so, for example,
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \AxiomC{$\Gamma, A \vdash B$}
+ \doubleLine\dashedLine
+ \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+produces the following:
+\begin{prooftree}
+ \AxiomC{$\Gamma, A \vdash B$}
+ \doubleLine\dashedLine
+ \UnaryInfC{$\Gamma \vdash A \rightarrow B$}
+\end{prooftree}
+There are corresponding global commands that can be placed anywhere in a proof and will affect all succeeding lines unless and until overridden.
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\alwaysNoLine=
+\item \verb=\alwaysSingleLine=
+\item \verb=\alwaysDoubleLine=
+\item \verb=\alwaysSolidLine=
+\item \verb=\alwaysDottedLine=
+\item \verb=\alwaysDashedLine=
+\end{description}
+\end{quote}
+Here `succeeding lines' means `succeeding in the (vertical) order that commands are given' not `logically succeeding'. (Note: Sam Buss comments that \verb=\alwaysNoLine= is `untested': but it seems to work fine on my trials.)
+
+So, for example, the commands
+\begin{quote}
+\begin{verbatim}
+\begin{prooftree}
+ \alwaysNoLine
+ \AxiomC{$\Pi_1$}
+ \UnaryInfC{$A$}
+ \AxiomC{[$A$]}
+ \UnaryInfC{$\Pi_2$}
+ \UnaryInfC{$B$}
+ \alwaysSingleLine
+ \UnaryInfC{$A \to B$}
+ \BinaryInfC{$B$}
+\end{prooftree}
+\end{verbatim}
+\end{quote}
+produces the following:
+\begin{prooftree}
+
+\alwaysNoLine
+\AxiomC{$\Pi_1$}
+\UnaryInfC{$A$}
+\AxiomC{[$A$]}
+\UnaryInfC{$\Pi_2$}
+\UnaryInfC{$B$}
+\alwaysSingleLine
+\UnaryInfC{$A \to B$}
+\BinaryInfC{$B$}
+\end{prooftree}
+
+\subsection{Turning a proof upside down}
+
+Suppose you want to set a proof-tree the other way up, i.e. get a \emph{downward} branching tree with the root at the \emph{top}. Then you need the command \verb=\rootAtTop=. Note, this applies only to the current proof. If you want to make this behaviour persistent, then use \verb=\alwaysRootAtTop=. (The default behaviour can be restored using \verb=\rootAtBottom= and \verb=\alwaysRootAtBottom=.)
+
+
+\section{Fine-tuning the proof layout}
+\texttt{bussproofs.sty} allows a lot of user-modification of the default style of proof lay-out, either by global modifications of parameters, or by local tweakings within a proof. We'll divide these commands into
+\begin{itemize}\setlength{\itemsep}{0.0in}
+\item commands for determining \emph{where a whole proof is set};
+\item commands for \emph{adjusting the `geometry' within a proof};
+\item commands for \emph{redefining line styles}.
+\end{itemize}
+
+\subsection{Where a proof is set}
+
+\noindent\textbf{i}\quad The amount of \emph{space above and below} a proof-tree display is set by the parameter
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\proofSkipAmount=
+\end{description}
+\end{quote}
+Its default setting is \verb={\vskip.8ex plus.8ex minus.4ex}=. This can be modified, and negative values of \verb=\vskip= are accepted.
+
+To change the space above the tree (which you'll want to do if the top lines are null axioms, which generate additional white space), use \verb=\def\proofSkipAmount{\vskip= \emph{new-skip}\verb=}= \emph{before} the opening command \verb=\begin{prooftree}=; the size of the skip after the proof can then be reset by another \verb=\def\proofSkipAmount{...}= command before the proof closes.
+
+\vspace{12pt}\noindent\textbf{ii}\quad Whole proofs set using the proof-tree environment can be \emph{nudged sideways} by using the command \verb=\hskip= \emph{nudge} (no brackets!) placed e.g. immediately after the command \verb=\begin{prooftree}=. A positive value of \emph{nudge} such as \verb=0.5in= shifts the proof to the right, a negative value such as \verb=-20pt= shifts the proof left.
+
+\EnableBpAbbreviations
+\vspace{4pt}\noindent\textbf{iii}\quad For \emph{vertical positioning of in-line proofs}, compare \AXC{$\phi \land \psi$}\UIC{$\phi$}\DP with \centerAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP and \bottomAlignProof\AXC{$\phi \land \psi$}\UIC{$\phi$}\DP\hspace{-6pt}. The first is set vertically centered within the current line (the default position), the second is set rather lower so (at least with a one-step proof) the inference line is on a level with the foot of the current line, and the third is set with the conclusion aligned to the current line. To produce the second tree, use the command \verb=\centerAlignProof=; to produce the third tree, use \verb=\bottomAlignProof=; to restore the default positioning
+use \verb=\normalAlignProof=.
+
+\subsection{Layout within a proof}
+In this section, we consider the use of
+
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\ScoreOverhang= (controls how far inference lines `overhang' the premisses/conclusion)
+\item \verb=\extraVskip= (controls the extra space above and below lines)
+\item \verb=\labelSpacing= (controls horizontal space separating labels and inference lines)
+\item \verb=\defaultHypSeparation= (controls horizontal spread of proof tree)
+\item \verb=\insertBetweenHyps= (can be used to adjust position of hypotheses in next inference)
+\item \verb=\kernHyps= (nudges hypotheses left or right)
+\end{description}
+\end{quote}
+
+\noindent\textbf{i}\quad The default setting of \verb=\ScoreOverhang= is \verb={4pt}=. This produces e.g. the tree
+\begin{prooftree}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\psi$}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\phi$}
+\BinaryInfC{$\psi \land \phi$}
+\end{prooftree}
+Inserting, for example, the line \verb=\def\ScoreOverhang{1pt}= at the beginning of the chain of proof-commands changes (improves!?) the look of the tree by reducing the `overhang' of inference lines:
+\begin{prooftree}
+\def\ScoreOverhang{1pt}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\psi$}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\phi$}
+\BinaryInfC{$\psi \land \phi$}
+\end{prooftree}
+\vspace{12pt}
+\noindent\textbf{ii}\quad The default setting of \verb=\extraVskip= is \verb={2pt}=, which inserts 2 pt spacing above and below an inference line, as in the last two proofs. To increase this throughout the proof, use e.g. the line \verb=\def\extraVskip{3pt}= at the beginning of the chain of proof-commands to get
+\begin{prooftree}
+\def\extraVskip{3pt}
+\def\ScoreOverhang{1pt}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\psi$}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\phi$}
+\BinaryInfC{$\psi \land \phi$}
+\end{prooftree}
+You can also change the interline skip on the fly, during a proof, to improve alignments. Thus compare
+\begin{center}
+\alwaysNoLine
+\AxiomC{$\Pi_1$}
+\UnaryInfC{$A$}
+\AxiomC{[$A$]}
+\UnaryInfC{$\Pi_2$}
+\UnaryInfC{$B$}
+\alwaysSingleLine
+\UnaryInfC{$A \to B$}
+\BinaryInfC{$B$}
+\DisplayProof
+\hspace{24pt}
+\alwaysNoLine
+\AxiomC{$\Pi_1$}
+\def\extraVskip{1pt}\UnaryInfC{$A$}
+\AxiomC{[$A$]}
+\def\extraVskip{2pt}
+\UnaryInfC{$\Pi_2$}
+\UnaryInfC{$B$}
+\def\extraVskip{2.5pt}
+\alwaysSingleLine
+\UnaryInfC{$A \to B$}
+\BinaryInfC{$B$}
+\DisplayProof
+\end{center}
+Here, the proof on the left was created by using the default settings, and the one on the right was created by the following commands (with the two proofs being set in the same line in a \verb=\begin{center} ... \end{center}= environment):
+\begin{quote}
+\begin{verbatim}
+\alwaysNoLine
+\AxiomC{$\Pi_1$}
+\def\extraVskip{1pt}
+\UnaryInfC{$A$}
+ \AxiomC{[$A$]}
+ \def\extraVskip{2pt}
+ \UnaryInfC{$\Pi_2$}
+ \UnaryInfC{$B$}
+ \def\extraVskip{2.5pt}
+ \alwaysSingleLine
+ \UnaryInfC{$A \to B$}
+ \BinaryInfC{$B$}
+\DisplayProof
+\end{verbatim}
+\end{quote}
+
+\vspace{4pt}
+\noindent\textbf{iii}\quad The default setting of \verb=\labelSpacing= is \verb={3pt}=, which inserts 3 pt between inference lines and their associated labels. To change this, use the command \verb=\def\labelSpacing{=\emph{new-space}\verb=}= at the beginning of a chain of proof-commands. For example
+\begin{prooftree}
+\def\extraVskip{2pt}
+\def\labelSpacing{8pt}
+\def\ScoreOverhang{1.2pt}
+\AxiomC{$(\phi \land \psi)$}
+\UnaryInfC{$\psi$}
+\AxiomC{}
+\RightLabel{\scriptsize(1)}
+\def\extraVskip{1pt}
+\UnaryInfC{$\neg\psi$}
+\def\extraVskip{2pt}
+\BinaryInfC{$\bot$}
+\RightLabel{\scriptsize(1)}
+\UnaryInfC{$\neg(\psi \land \phi)$}
+\end{prooftree}
+is set with \verb=\def\labelSpacing{8pt}=.
+
+
+
+
+\vspace{12pt}
+
+\noindent\textbf{iv}\quad The default setting of \verb=\defaultHypSeparation= is \verb={\hskip.2in}=. Increase this to spread out a spread out a proof horizontally, decrease it to squeeze the proof. Thus compare
+\begin{center}
+\def\defaultHypSeparation{\hskip .1in}
+\def\ScoreOverhang{1pt}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\psi$}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\phi$}
+\BinaryInfC{$\psi \land \phi$}
+\DisplayProof
+\hspace{24pt}
+\def\defaultHypSeparation{\hskip.5in}
+\def\ScoreOverhang{1pt}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\psi$}
+\AxiomC{$\phi \land \psi$}
+\UnaryInfC{$\phi$}
+\BinaryInfC{$\psi \land \phi$}
+\DisplayProof
+\end{center}
+where the proof commands for the left tree start \verb=\def\defaultHypSeparation{\hskip .1in}=, and for the right tree start \verb=\def\defaultHypSeparation{\hskip .5in}=.
+
+\vspace{12pt}
+\noindent\textbf{v}\quad Use the command \verb=\insertBetweenHyps{=\emph{stuff}\verb=}= before a binary or trinary inference command to insert \emph{stuff} between the hypotheses of that inference. The obvious use of this is to adjust the spacing between the hypotheses of that inference, by using e.g.
+\verb=\insertBetweenHyps{\hskip -4pt}=.
+
+\vspace{12pt}
+\noindent\textbf{vi}\quad Use the command \verb=\kernHyps{=\emph{kern}\verb=}= before an inference command to nudge the hypotheses of that inference right by the distance \emph{kern}, e.g. \verb=4pt=. Negative values of \emph{kern} nudge the hypotheses to the left.
+
+\subsection{Inference-line styles}
+
+In this section, we consider the use of
+
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\ruleScoreFiller= (sets the style of solid rules)
+\item \verb=\dottedScoreFiller= (sets the style of dotted rules)
+\item \verb=\dashedBuildScore= (sets the style of dashed rules)
+\end{description}
+\end{quote}
+\noindent\textbf{i}\quad The default setting of \verb=\ruleScoreFiller= is \verb={\hrule}=, and in \LaTeX\ an unqualified \verb=\hrule= command produces a horizontal line of thickness 0.4 pt. To change the rule's thickness, use the command \verb=\def\ruleScoreFiller{\hrule height= \emph{new-thickness}\verb=}=.
+
+\vspace{12pt}
+\noindent\textbf{ii}\quad The default setting of \verb=\dottedScoreFiller= is \verb={\hbox to4pt{\hss.\hss}}=. The default for \verb=\dashedBuildScore= is \begin{quote}
+\verb={\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}=
+\end{quote} Both defaults can be altered to produce any other desired type of line.
+
+\section{Abbreviating the commands}\label{abbrev}
+Using the command \verb=\EnableBpAbbreviations= enables some laconic shorthand for various commands:
+\begin{quote}
+\begin{description}\setlength{\itemsep}{0.0in}
+\item \verb=\AX= and \verb=\AXC= abbreviate \verb=\Axiom= and \verb=\AxiomC=
+\item \verb=\UI= and \verb=\UIC= abbreviate \verb=\UnaryInf= and \verb=\UnaryInfC=
+\item \verb=\BI= and \verb=\BIC= abbreviate \verb=\BinaryInf= and \verb=\BinaryInfC=
+\item \verb=\TI= and \verb=\TIC= abbreviate \verb=\TrinaryInf= and \verb=\TrinaryInfC=
+\item \verb=\DP= abbreviates \verb=\DisplayProof=
+\end{description}
+\end{quote}
+The enabling of these short abbreviations is optional, and users should guard against conflicts with commands from other
+macro packages or their own defined abbreviations.
+
+\end{document}
diff --git a/macros/latex/contrib/bussproofs/README b/macros/latex/contrib/bussproofs/README
new file mode 120000
index 0000000000..c3ca07460a
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/README
@@ -0,0 +1 @@
+README.txt \ No newline at end of file
diff --git a/macros/latex/contrib/bussproofs/README.txt b/macros/latex/contrib/bussproofs/README.txt
new file mode 100644
index 0000000000..8690625e9a
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/README.txt
@@ -0,0 +1,31 @@
+bussproofs, version 1.1.
+
+Proof trees in the style of the sequent calculus and other proof systems.
+
+The package allows the construction of proof trees in the style of
+the sequent calculus and many other proof systems. One novel
+feature of the macros is they support the horizontal alignment
+according to some centre point specified with the command \fCenter.
+This is the style often used in sequent calculus proofs.
+
+The package works in a Plain TeX document, as well as in LaTeX; an
+exposition of the commands available is given in the package file
+itself. Documentation is also given in a separate LaTeX/FILE,
+BussGuide2.tex/BussGuide2.pdf.
+
+Distribution under the LaTeX Project Public License
+
+The CTAN distribution includes:
+
+bussproofs.sty - version 1.1 of the style files.
+
+BussGuide2.pdf - The documentation by Peter Smith.
+BussGuide2.tex - LaTeX source for the documentation.
+
+testbp2.tex - A file used for testing, with examples of usage.
+testbp2.pdf - The output of the testbp2.tex
+
+README.txt - This file.
+
+Maintained by Sam Buss
+sbuss@math.ucsd.edu
diff --git a/macros/latex/contrib/bussproofs/bussproofs.sty b/macros/latex/contrib/bussproofs/bussproofs.sty
new file mode 100644
index 0000000000..d5b46d389c
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/bussproofs.sty
@@ -0,0 +1,1137 @@
+%
+\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
+% bussproofs.sty. Version 1.1
+% (c) 1994,1995,1996,2004,2005,2006, 2011.
+% Copyright retained by Samuel R. Buss.
+%
+% ==== Legal statement: ====
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% http://www.latex-project.org/lppl.txt.
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/1 or later.
+%
+% This work has the LPPL maintenance status 'maintained'.
+%
+% The Current Maintainer of the work is Sam Buss.
+%
+% This work consists of bussproofs.sty.
+% =====
+% Informal summary of legal situation:
+% This software may be used and distributed freely, except that
+% if you make changes, you must change the file name to be different
+% than bussproofs.sty to avoid compatibility problems.
+% The terms of the LaTeX Public License are the legally controlling terms
+% and override any contradictory terms of the "informal situation".
+%
+% Please report comments and bugs to sbuss@ucsd.edu.
+%
+% Thanks to Felix Joachimski for making changes to let these macros
+% work in plain TeX in addition to LaTeX. Nothing has been done
+% to see if they work in AMSTeX. The comments below mostly
+% are written for LaTeX, however.
+% July 2004, version 0.7
+% - bug fix, right labels with descenders inserted too much space.
+% Thanks to Peter Smith for finding this bug,
+% see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
+% March 2005, version 0.8.
+% Added a default definition for \fCenter at Denis Kosygin's
+% suggestion.
+% September 2005, version 0.9.
+% Fixed some subtle spacing problems, by adding %'s to the end of
+% few lines where they were inadvertantly omitted. Thanks to
+% Arnold Beckmann for finding and fixing this problem.
+% April 2006, version 0.9.1. Updated comments and testbp2.tex file.
+% No change to the actual macros.
+% June 2006, version 1.0. The first integer numbered release.
+% New feature: root of proof may now be at the bottom instead of
+% at just the top. Thanks to Alex Hertel for the suggestion to implement
+% this.
+% June 2011, version 1.1.
+% New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann
+% for taking the initiative to implement these.
+% Four new commands: QuaternaryInf(C) and QuinaryInf(C).
+% Bug fix: \insertBetweenHyps now works for proofs with root at top and
+% three or more hypotheses..
+
+% A good exposition of how to use bussproofs.sty (version 0.9) has been written
+% by Peter Smith and is available on the internet and in the CTAN
+% distribution.
+% The comments below also describe the features of bussproofs.sty,
+% including user-modifiable parameters.
+
+% bussproofs.sty allows the construction of proof trees in the
+% style of the sequent calculus and many other proof systems
+% One novel feature of these macros is they support the horizontal
+% alignment according to some center point specified with the
+% command \fCenter. This is the style often used in sequent
+% calculus proofs.
+% Proofs are specified in left-to-right traversal order.
+% For example a proof
+% A B
+% -----
+% D C
+% ---------
+% E
+%
+% if given in the order D,A,B,C,E. Each line in the proof is
+% specified according to the arity of the inference which generates
+% it. Thus, E would be specified with a \BinaryInf or \BinaryInfC
+% command.
+%
+% The above proof tree could be displayed with the commands:
+%
+% \AxiomC{D}
+% \AxiomC{A}
+% \AxiomC{B}
+% \BinaryInfC{C}
+% \BinaryInfC{E}
+% \DisplayProof
+%
+% Inferences in a proof may be nullary (axioms), unary, binary, or
+% trinary.
+%
+% IMPORTANT: You must give the \DisplayProof command to make the proof
+% be printed. To display a centered proof on a line by itself,
+% put the proof inside \begin{center} ... \end{center}.
+%
+% There are two styles for specifying horizontal centering of
+% lines (formulas or sequents) in a proof. One format \AxiomC{...}
+% just centers the formula {...} in the usual way. The other
+% format is \Axiom$...\fCenter...$. Here, the \fCenter specifies
+% the center of the formula. (It is permissable for \fCenter to
+% generate typeset material; in fact, I usually define it to generate
+% the sequent arrow.) In unary inferences, the \fCenter
+% positions will be vertically aligned in the upper and lower lines of
+% the inference. Unary, Binary, Trinary inferences are specified
+% with the same format as Axioms. The two styles of centering
+% lines may be combined in a single proof.
+%
+% By using the optional \EnableBpAbbreviations command, various
+% abbreviated two or three letter commands are enabled. This allows,
+% in particular:
+% \AX and \AXC for \Axiom and \AxiomC, (resp.),
+% \DP for \DisplayProof,
+% \BI and \BIC for \BinaryInf and \BinaryInfC,
+% \UI and \UIC for \UnaryInf and \UnaryInfC,
+% \TI and \TIC for \TrinaryInf and \TrinaryInfC,
+% \LL and \RL for \LeftLabel and \RightLabel.
+% See the source code below for additional abbreviations.
+% The enabling of these short abbreviations is OPTIONAL, since
+% there is the possibility of conflicting with names from other
+% macro packages.
+%
+% By default, the inferences have single horizontal lines (scores)
+% This can be overridden using the \doubleLine, \noLine commands.
+% These two commands affect only the next inference. You can make
+% make a permanent override that applies to the rest of the current
+% proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine
+% and \alwaysSingleLine work in the analogous way.
+%
+% The macros do their best to give good placements of for the
+% parts of the proof. Several macros allow you to override the
+% defaults. These are \insertBetweenHyps{...} which overrides
+% the default spacing between hypotheses of Binary and Trinary
+% inferences with {...}. And \kernHyps{...} specifies a distance
+% to shift the whole block of hypotheses to the right (modifying
+% the default center position.
+% Other macros set the vertical placement of the whole proof.
+% The default is to try to do a good job of placement for inferences
+% included in text. Two other useful macros are: \bottomAlignProof
+% which aligns the hbox output by \DisplayProof according to the base
+% of the bottom line of the proof, and \centerAlignProof which
+% does a precise center vertical alignment.
+%
+% Often, one wishes to place a label next to an inference, usually
+% to specify the type of inference. These labels can be placed
+% by using the commands \LeftLabel{...} and \RightLabel{...}
+% immediately before the command which specifies the inference.
+% For example, to generate
+%
+% A B
+% --------- X
+% C
+%
+% use the commands
+% \AxiomC{A}
+% \AxiomC{B}
+% \RightLabel{X}
+% \BinaryInfC{C}
+% \DisplayProof
+%
+% The \DisplayProof command just displays the proof as a text
+% item. This allows you to put proofs anywhere normal text
+% might appear; for example, in a paragraph, in a table, in
+% a tabbing environment, etc. When displaying a proof as inline text,
+% you should write \DisplayProof{} (with curly brackets) so that
+% LaTeX will not "eat" the white space following the \DisplayProof
+% command.
+% For displaying proofs in a centered display: Do not use the \[...\]
+% construction (nor $$...$$). Instead use
+% \begin{center} ... \DisplayProof\end{center}.
+% Actually there is a better construction to use instead of the
+% \begin{center}...\DisplayProof\end{center}. This is to
+% write
+% \begin{prooftree} ... \end{prooftree}.
+% Note there is no \DisplayProof used for this: the
+% \end{prooftree} automatically supplies the \DisplayProof
+% command.
+%
+% Warning: Any commands that set line types or set vertical or
+% horizontal alignment that are given AFTER the \DisplayProof
+% command will affect the next proof, no matter how distant.
+
+
+
+
+% Usages:
+% =======
+%
+% \Axiom$<antecedent>\fCenter<succedent>$
+%
+% \AxiomC{<whole sequent or formula}
+%
+% Note that the use of surrounding {}'s is mandatory in \AxiomC and
+% is prohibited in $\Axiom. On the other hand, the $'s are optional
+% in \AxiomC and are mandatory in \Axiom. To typeset the argument
+% to \AxiomC in math mode, you must use $'s (or \(...\) ).
+% The same comments apply to the inference commands below.
+%
+% \UnaryInf$<antecendent>\fCenter<succedent>$
+%
+% \UnaryInfC{<whole sequent or formula>}
+%
+% \BinaryInf$<antecendent>\fCenter<succedent>$
+%
+% \BinaryInfC{<whole sequent or formula>}
+%
+% \TrinaryInf$<antecendent>\fCenter<succedent>$
+%
+% \TrinaryInfC{<whole sequent or formula>}
+%
+% \QuaternaryInf$<antecendent>\fCenter<succedent>$
+%
+% \QuaternaryInfC{<whole sequent or formula>}
+%
+% \QuinaryInf$<antecendent>\fCenter<succedent>$
+%
+% \QuinaryInfC{<whole sequent or formula>}
+%
+% \LeftLabel{<text>} - Puts <text> as a label to the left
+% of the next inference line. (Works even if
+% \noLine is used too.)
+%
+% \RightLabel{<text>} - Puts <text> as a label to the right of the
+% next inference line. (Also works with \noLine.)
+%
+% \DisplayProof - outputs the whole proof tree (and finishes it).
+% The proof tree is output as an hbox.
+%
+%
+% \kernHyps{<dimen>} - Slides the upper hypotheses right distance <dimen>
+% (This is similar to shifting conclusion left)
+% - kernHyps works with Unary, Binary and Trinary
+% inferences and with centered or uncentered sequents.
+% - Negative values for <dimen> are permitted.
+%
+% \insertBetweenHyps{...} - {...} will be inserted between the upper
+% hypotheses of a Binary or Trinary Inferences.
+% It is possible to use negative horizontal space
+% to push them closer together (and even overlap).
+% This command affects only the next inference.
+%
+% \doubleLine - Makes the current (ie, next) horizontal line doubled
+%
+% \alwaysDoubleLine - Makes lines doubled for rest of proof
+%
+% \singleLine - Makes the current (ie, next) line single
+%
+% \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine.
+%
+% \noLine - Make no line at all at current (ie next) inference.
+%
+% \alwaysNoLine - Makes no lines for rest of proof. (Untested)
+%
+% \solidLine - Does solid horizontal line for current inference
+%
+% \dottedLine - Does dotted horizontal line for current inference
+%
+% \dashedLine - Does dashed horizontal line for current inference
+%
+% \alwaysSolidLine - Makes the indicated change in line type, permanently
+% \alwaysDashedLine until end of proof or until overridden.
+% \alwaysDottedLine
+%
+% \bottomAlignProof - Vertically align proof according to its bottom line.
+% \centerAlignProof - Vertically align proof proof precisely in its center.
+% \normalAlignProof - Overrides earlier bottom/center AlignProof commands.
+% The default alignment will look good in most cases,
+% whether the proof is displayed or is
+% in-line. Other alignments may be more
+% appropriate when putting proofs in tables or
+% pictures, etc. For custom alignments, use
+% TeX's raise commands.
+%
+% \rootAtTop - specifies that proofs have their root a the top. That it,
+% proofs will be "upside down".
+% \rootAtBottom - (default) Specifies that proofs have root at the bottom
+% The \rootAtTop and \rootAtBottom commands apply *only* to the
+% current proof. If you want to make them persistent, use one of
+% the next two commands:
+% \alwaysRootAtTop
+% \alwaysRootAtBottom (default)
+%
+
+% Optional short abbreviations for commands:
+\def\EnableBpAbbreviations{%
+ \let\AX\Axiom
+ \let\AXC\AxiomC
+ \let\UI\UnaryInf
+ \let\UIC\UnaryInfC
+ \let\BI\BinaryInf
+ \let\BIC\BinaryInfC
+ \let\TI\TrinaryInf
+ \let\TIC\TrinaryInfC
+ \let\QI\QuaternaryInf
+ \let\QIC\QuaternaryInfC
+ \let\QuI\QuinaryInf
+ \let\QuIC\QuinaryInfC
+ \let\LL\LeftLabel
+ \let\RL\RightLabel
+ \let\DP\DisplayProof
+}
+
+% Parameters which control the style of the proof trees.
+% The user may wish to override these parameters locally or globally.
+% BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
+% future incompatibilities). Instead, you should change them in your
+% TeX document right after including this style file in the
+% header material of your LaTeX document.
+
+\def\ScoreOverhang{4pt} % How much underlines extend out
+\def\ScoreOverhangLeft{\ScoreOverhang}
+\def\ScoreOverhangRight{\ScoreOverhang}
+
+\def\extraVskip{2pt} % Extra space above and below lines
+\def\ruleScoreFiller{\hrule} % Horizontal rule filler.
+\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}}
+\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}
+\def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler.
+\def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start.
+
+\def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given
+
+\def\labelSpacing{3pt} % Horizontal space separating labels and lines
+
+\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex}
+ % Space above and below a prooftree display.
+
+\def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom
+%\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down
+
+\ifx\fCenter\undefined
+\def\fCenter{\relax}
+\fi
+
+%
+% End of user-modifiable parameters.
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Here are some internal paramenters and defaults. Not really intended
+% to be user-modifiable.
+
+\def\theHypSeparation{\defaultHypSeparation}
+\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler.
+\def\alwaysBuildScore{\defaultBuildScore}
+\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler.
+\def\buildScore{\alwaysBuildScore} %This command builds the score.
+\def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses.
+
+\def\defaultLeftLabel{}
+\def\defaultRightLabel{}
+
+\def\myTrue{Y}
+\def\bottomAlignFlag{N}
+\def\centerAlignFlag{N}
+\def\defaultRootAtBottomFlag{Y}
+\def\rootAtBottomFlag{Y}
+
+% End of internal parameters and defaults.
+
+\expandafter\ifx\csname newenvironment\endcsname\relax%
+% If in TeX:
+\message{\BPmessage}
+\def\makeatletter{\catcode`\@=11\relax}
+\def\makeatother{\catcode`\@=12\relax}
+\makeatletter
+\def\newcount{\alloc@0\count\countdef\insc@unt}
+\def\newdimen{\alloc@1\dimen\dimendef\insc@unt}
+\def\newskip{\alloc@2\skip\skipdef\insc@unt}
+\def\newbox{\alloc@4\box\chardef\insc@unt}
+\makeatother
+\else
+% If in LaTeX
+\typeout{\BPmessage}
+\newenvironment{prooftree}%
+{\begin{center}\proofSkipAmount \leavevmode}%
+{\DisplayProof \proofSkipAmount \end{center} }
+\fi
+
+\def\thecur#1{\csname#1\number\theLevel\endcsname}
+
+\newcount\theLevel % This counter is the height of the stack.
+\global\theLevel=0 % Initialized to zero
+\newcount\myMaxLevel
+\global\myMaxLevel=0
+\newbox\myBoxA % Temporary storage boxes
+\newbox\myBoxB
+\newbox\myBoxC
+\newbox\myBoxD
+\newbox\myBoxLL % Boxes for the left label and the right label.
+\newbox\myBoxRL
+\newdimen\thisAboveSkip %Internal use: amount to skip above line
+\newdimen\thisBelowSkip %Internal use: amount to skip below line
+\newdimen\newScoreStart % More temporary storage.
+\newdimen\newScoreEnd
+\newdimen\newCenter
+\newdimen\displace
+\newdimen\leftLowerAmt% Amount to lower left label
+\newdimen\rightLowerAmt% Amount to lower right label
+\newdimen\scoreHeight% Score height
+\newdimen\scoreDepth% Score Depth
+\newdimen\htLbox%
+\newdimen\htRbox%
+\newdimen\htRRbox%
+\newdimen\htRRRbox%
+\newdimen\htAbox%
+\newdimen\htCbox%
+
+\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
+\setbox\myBoxRL=\hbox{\defaultRightLabel}%
+
+\def\allocatemore{%
+ \ifnum\theLevel>\myMaxLevel%
+ \expandafter\newbox\curBox%
+ \expandafter\newdimen\curScoreStart%
+ \expandafter\newdimen\curCenter%
+ \expandafter\newdimen\curScoreEnd%
+ \global\advance\myMaxLevel by1%
+ \fi%
+}
+
+\def\prepAxiom{%
+ \advance\theLevel by1%
+ \edef\curBox{\thecur{myBox}}%
+ \edef\curScoreStart{\thecur{myScoreStart}}%
+ \edef\curCenter{\thecur{myCenter}}%
+ \edef\curScoreEnd{\thecur{myScoreEnd}}%
+ \allocatemore%
+}
+
+\def\Axiom$#1\fCenter#2${%
+ % Get level and correct names set.
+ \prepAxiom%
+ % Define the boxes
+ \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
+ \setbox\myBoxB=\hbox{$#2$}%
+ \global\setbox\curBox=%
+ \hbox{\hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+ % Set the relevant dimensions for the boxes
+ \global\curScoreStart=0pt \relax
+ \global\curScoreEnd=\wd\curBox \relax
+ \global\curCenter=\wd\myBoxA \relax
+ \global\advance \curCenter by \ScoreOverhangLeft%
+ \ignorespaces
+}
+
+\def\AxiomC#1{ % Note argument not in math mode
+ % Get level and correct names set.
+ \prepAxiom%
+ % Define the box.
+ \setbox\myBoxA=\hbox{#1}%
+ \global\setbox\curBox =%
+ \hbox{\hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
+ % Set the relevant dimensions for the boxes
+ \global\curScoreStart=0pt \relax
+ \global\curScoreEnd=\wd\curBox \relax
+ \global\curCenter=.5\wd\curBox \relax
+ \global\advance \curCenter by \ScoreOverhangLeft%
+ \ignorespaces
+}
+
+\def\prepUnary{%
+ \ifnum \theLevel<1
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\curBox{\thecur{myBox}}%
+ \edef\curScoreStart{\thecur{myScoreStart}}%
+ \edef\curCenter{\thecur{myCenter}}%
+ \edef\curScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\UnaryInf$#1\fCenter#2${%
+ \prepUnary%
+ \buildConclusion{#1}{#2}%
+ \joinUnary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\UnaryInfC#1{
+ \prepUnary%
+ \buildConclusionC{#1}%
+ %Align and join the curBox and the new box into one vbox.
+ \joinUnary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\prepBinary{%
+ \ifnum\theLevel<2
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\BinaryInf$#1\fCenter#2${%
+ \prepBinary%
+ \buildConclusion{#1}{#2}%
+ \joinBinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\BinaryInfC#1{%
+ \prepBinary%
+ \buildConclusionC{#1}%
+ \joinBinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\prepTrinary{%
+ \ifnum\theLevel<3
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
+ \edef\ccurScoreStart{\thecur{myScoreStart}}%
+ \edef\ccurCenter{\thecur{myCenter}}%
+ \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\TrinaryInf$#1\fCenter#2${%
+ \prepTrinary%
+ \buildConclusion{#1}{#2}%
+ \joinTrinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\TrinaryInfC#1{%
+ \prepTrinary%
+ \buildConclusionC{#1}%
+ \joinTrinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\prepQuaternary{%
+ \ifnum\theLevel<4
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
+ \edef\rrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrcurCenter{\thecur{myCenter}}%
+ \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
+ \edef\ccurScoreStart{\thecur{myScoreStart}}%
+ \edef\ccurCenter{\thecur{myCenter}}%
+ \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\QuaternaryInf$#1\fCenter#2${%
+ \prepQuaternary%
+ \buildConclusion{#1}{#2}%
+ \joinQuaternary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\QuaternaryInfC#1{%
+ \prepQuaternary%
+ \buildConclusionC{#1}%
+ \joinQuaternary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\joinQuaternary{% Construct the quarterary inference into a vbox.
+ % Join the four hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rrcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\rcurBox%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\ccurBox%
+ \advance\lcurScoreEnd by3\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
+ \unhcopy\myBoxA\box\rcurBox
+ \unhcopy\myBoxA\box\rrcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htCbox = \ht\ccurBox%
+ \htRbox = \ht\rcurBox%
+ \htRRbox = \ht\rrcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\prepQuinary{%
+ \ifnum\theLevel<5
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis
+ \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrrcurCenter{\thecur{myCenter}}%
+ \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
+ \edef\rrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrcurCenter{\thecur{myCenter}}%
+ \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
+ \edef\ccurScoreStart{\thecur{myScoreStart}}%
+ \edef\ccurCenter{\thecur{myCenter}}%
+ \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\QuinaryInf$#1\fCenter#2${%
+ \prepQuinary%
+ \buildConclusion{#1}{#2}%
+ \joinQuinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\QuinaryInfC#1{%
+ \prepQuinary%
+ \buildConclusionC{#1}%
+ \joinQuinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\joinQuinary{% Construct the quinary inference into a vbox.
+ % Join the five hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rrrcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\rrcurBox%
+ \advance\lcurScoreEnd by\wd\rcurBox%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\ccurBox%
+ \advance\lcurScoreEnd by4\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
+ \unhcopy\myBoxA\box\rcurBox
+ \unhcopy\myBoxA\box\rrcurBox
+ \unhcopy\myBoxA\box\rrrcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htCbox = \ht\ccurBox%
+ \htRbox = \ht\rcurBox%
+ \htRRbox = \ht\rrcurBox%
+ \htRRRbox = \ht\rrrcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
+ % Define the boxes
+ \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
+ \setbox\myBoxB=\hbox{$#2$}%
+ % Put them together in \myBoxC
+ \setbox\myBoxC =%
+ \hbox{\hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+ % Calculate the center of the \myBoxC string.
+ \newScoreStart=0pt \relax%
+ \newCenter=\wd\myBoxA \relax%
+ \advance \newCenter by \ScoreOverhangLeft%
+ \newScoreEnd=\wd\myBoxC%
+}
+
+\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
+ % Define the box.
+ \setbox\myBoxA=\hbox{#1}%
+ \setbox\myBoxC =%
+ \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
+ % Calculate kerning to line up centers
+ \newScoreStart=0pt \relax%
+ \newCenter=.5\wd\myBoxC \relax%
+ \newScoreEnd=\wd\myBoxC%
+ \advance \newCenter by \ScoreOverhangLeft%
+}
+
+\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox
+ \global\advance\curCenter by -\hypKernAmt%
+ \ifnum\curCenter<\newCenter%
+ \displace=\newCenter%
+ \advance \displace by -\curCenter%
+ \kernUpperBox%
+ \else%
+ \displace=\curCenter%
+ \advance \displace by -\newCenter%
+ \kernLowerBox%
+ \fi%
+ \ifnum \newScoreStart < \curScoreStart %
+ \global \curScoreStart = \newScoreStart \fi%
+ \ifnum \curScoreEnd < \newScoreEnd %
+ \global \curScoreEnd = \newScoreEnd \fi%
+ % Leave room for the left label.
+ \ifnum \curScoreStart<\wd\myBoxLL%
+ \global\displace = \wd\myBoxLL%
+ \global\advance\displace by -\curScoreStart%
+ \kernUpperBox%
+ \kernLowerBox%
+ \fi%
+ % Draw the score
+ \buildScore%
+ % Form the score and labels into a box.
+ \buildScoreLabels%
+ % Form the new box and its dimensions
+ \ifx\rootAtBottomFlag\myTrue%
+ \buildRootBottom%
+ \else%
+ \buildRootTop%
+ \fi%
+ \global \curScoreStart=\newScoreStart%
+ \global \curScoreEnd=\newScoreEnd%
+ \global \curCenter=\newCenter%
+}
+
+\def\buildRootBottom{%
+ \global \setbox \curBox =%
+ \vbox{\box\curBox%
+ \vskip\thisAboveSkip \relax%
+ \nointerlineskip\box\myBoxD%
+ \vskip\thisBelowSkip \relax%
+ \nointerlineskip\box\myBoxC}%
+}
+
+\def\buildRootTop{%
+ \global \setbox \curBox =%
+ \vbox{\box\myBoxC%
+ \vskip\thisAboveSkip \relax%
+ \nointerlineskip\box\myBoxD%
+ \vskip\thisBelowSkip \relax%
+ \nointerlineskip\box\curBox}%
+}
+
+\def\kernUpperBox{%
+ \global\setbox\curBox =%
+ \hbox{\hskip\displace\box\curBox}%
+ \global\advance \curScoreStart by \displace%
+ \global\advance \curScoreEnd by \displace%
+ \global\advance\curCenter by \displace%
+}
+
+\def\kernLowerBox{%
+ \global\setbox\myBoxC =%
+ \hbox{\hskip\displace\unhbox\myBoxC}%
+ \global\advance \newScoreStart by \displace%
+ \global\advance \newScoreEnd by \displace%
+ \global\advance\newCenter by \displace%
+}
+
+\def\joinBinary{% Construct the binary inference into a vbox.
+ % Join the two hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htRbox = \ht\rcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+\def\joinTrinary{% Construct the trinary inference into a vbox.
+ % Join the three hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\ccurBox%
+ \advance\lcurScoreEnd by2\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
+ \unhcopy\myBoxA\box\rcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htCbox = \ht\ccurBox%
+ \htRbox = \ht\rcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+\def\DisplayProof{%
+ % Display (and purge) the proof tree.
+ % Choose the appropriate vertical alignment.
+ \ifnum \theLevel=1 \relax \else%x
+ \errmessage{Proof tree badly specified.}%
+ \fi%
+ \edef\curBox{\thecur{myBox}}%
+ \ifx\bottomAlignFlag\myTrue%
+ \displace=0pt%
+ \else%
+ \displace=.5\ht\curBox%
+ \ifx\centerAlignFlag\myTrue\relax
+ \else%
+ \advance\displace by -3pt%
+ \fi%
+ \fi%
+ \leavevmode%
+ \lower\displace\hbox{\copy\curBox}%
+ \global\theLevel=0%
+ \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always"
+ \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always"
+ \global\def\bottomAlignFlag{N}%
+ \global\def\centerAlignFlag{N}%
+ \resetRootPosition
+ \resetInferenceDefaults%
+ \ignorespaces
+}
+
+\def\buildSingleScore{% Make an hbox with a single score.
+ \displace=\curScoreEnd%
+ \advance \displace by -\curScoreStart%
+ \global\setbox \myBoxD =%
+ \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}%
+ %\global\setbox \myBoxD =%
+ %\hbox{\hskip\curScoreStart\relax \box\myBoxD}%
+}
+
+\def\buildDoubleScore{% Make an hbox with a double score.
+ \buildSingleScore%
+ \global\setbox\myBoxD=%
+ \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}%
+}
+
+\def\buildNoScore{% Make an hbox with no score (raise a little anyway)
+ \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}%
+}
+
+\def\doubleLine{%
+ \gdef\buildScore{\buildDoubleScore}% Set next score to this type
+ \ignorespaces
+}
+\def\alwaysDoubleLine{%
+ \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof.
+ \gdef\buildScore{\buildDoubleScore}% Set next score to be double
+ \ignorespaces
+}
+\def\singleLine{%
+ \gdef\buildScore{\buildSingleScore}% Set next score to be single
+ \ignorespaces
+}
+\def\alwaysSingleLine{%
+ \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof.
+ \gdef\buildScore{\buildSingleScore}% Set next score to be single
+ \ignorespaces
+}
+\def\noLine{%
+ \gdef\buildScore{\buildNoScore}% Set next score to this type
+ \ignorespaces
+}
+\def\alwaysNoLine{%
+ \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof.
+ \gdef\buildScore{\buildNoScore}% Set next score to be blank
+ \ignorespaces
+}
+\def\solidLine{%
+ \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
+ \ignorespaces
+}
+\def\alwaysSolidLine{%
+ \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof
+ \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
+ \ignorespaces
+}
+\def\dottedLine{%
+ \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
+ \ignorespaces
+}
+\def\alwaysDottedLine{%
+ \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof
+ \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
+ \ignorespaces
+}
+\def\dashedLine{%
+ \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
+ \ignorespaces
+}
+\def\alwaysDashedLine{%
+ \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof
+ \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
+ \ignorespaces
+}
+\def\kernHyps#1{%
+ \gdef\hypKernAmt{#1}%
+ \ignorespaces
+}
+\def\insertBetweenHyps#1{%
+ \gdef\theHypSeparation{#1}%
+ \ignorespaces
+}
+
+\def\centerAlignProof{%
+ \def\centerAlignFlag{Y}%
+ \def\bottomAlignFlag{N}%
+ \ignorespaces
+}
+\def\bottomAlignProof{%
+ \def\centerAlignFlag{N}%
+ \def\bottomAlignFlag{Y}%
+ \ignorespaces
+}
+\def\normalAlignProof{%
+ \def\centerAlignFlag{N}%
+ \def\bottomAlignFlag{N}%
+ \ignorespaces
+}
+
+\def\LeftLabel#1{%
+ \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}%
+ \ignorespaces
+}
+\def\RightLabel#1{%
+ \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}%
+ \ignorespaces
+}
+
+\def\buildScoreLabels{%
+ \scoreHeight = \ht\myBoxD%
+ \scoreDepth = \dp\myBoxD%
+ \leftLowerAmt=\ht\myBoxLL%
+ \advance \leftLowerAmt by -\dp\myBoxLL%
+ \advance \leftLowerAmt by -\scoreHeight%
+ \advance \leftLowerAmt by \scoreDepth%
+ \leftLowerAmt=.5\leftLowerAmt%
+ \rightLowerAmt=\ht\myBoxRL%
+ \advance \rightLowerAmt by -\dp\myBoxRL%
+ \advance \rightLowerAmt by -\scoreHeight%
+ \advance \rightLowerAmt by \scoreDepth%
+ \rightLowerAmt=.5\rightLowerAmt%
+ \displace = \curScoreStart%
+ \advance\displace by -\wd\myBoxLL%
+ \global\setbox\myBoxD =%
+ \hbox{\hskip\displace%
+ \lower\leftLowerAmt\copy\myBoxLL%
+ \box\myBoxD%
+ \lower\rightLowerAmt\copy\myBoxRL}%
+ \global\thisAboveSkip = \ht\myBoxLL%
+ \global\advance \thisAboveSkip by -\leftLowerAmt%
+ \global\advance \thisAboveSkip by -\scoreHeight%
+ \ifnum \thisAboveSkip<0 %
+ \global\thisAboveSkip=0pt%
+ \fi%
+ \displace = \ht\myBoxRL%
+ \advance \displace by -\rightLowerAmt%
+ \advance \displace by -\scoreHeight%
+ \ifnum \displace<0 %
+ \displace=0pt%
+ \fi%
+ \ifnum \displace>\thisAboveSkip %
+ \global\thisAboveSkip=\displace%
+ \fi%
+ \global\thisBelowSkip = \dp\myBoxLL%
+ \global\advance\thisBelowSkip by \leftLowerAmt%
+ \global\advance\thisBelowSkip by -\scoreDepth%
+ \ifnum\thisBelowSkip<0 %
+ \global\thisBelowSkip = 0pt%
+ \fi%
+ \displace = \dp\myBoxRL%
+ \advance\displace by \rightLowerAmt%
+ \advance\displace by -\scoreDepth%
+ \ifnum\displace<0 %
+ \displace = 0pt%
+ \fi%
+ \ifnum\displace>\thisBelowSkip%
+ \global\thisBelowSkip = \displace%
+ \fi%
+ \global\thisAboveSkip = -\thisAboveSkip%
+ \global\thisBelowSkip = -\thisBelowSkip%
+ \global\advance\thisAboveSkip by\extraVskip% Extra space above line
+ \global\advance\thisBelowSkip by\extraVskip% Extra space below line
+}
+
+\def\resetInferenceDefaults{%
+ \global\def\theHypSeparation{\defaultHypSeparation}%
+ \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
+ \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
+ \global\def\buildScore{\alwaysBuildScore}%
+ \global\def\theScoreFiller{\alwaysScoreFiller}%
+ \gdef\hypKernAmt{0pt}% Restore to zero kerning.
+}
+
+
+\def\rootAtBottom{%
+ \global\def\rootAtBottomFlag{Y}%
+}
+
+\def\rootAtTop{%
+ \global\def\rootAtBottomFlag{N}%
+}
+
+\def\resetRootPosition{%
+ \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag}
+}
+
+\def\alwaysRootAtBottom{%
+ \global\def\defaultRootAtBottomFlag{Y}
+ \rootAtBottom
+}
+
+\def\alwaysRootAtTop{%
+ \global\def\defaultRootAtBottomFlag{N}
+ \rootAtTop
+}
+
+
diff --git a/macros/latex/contrib/bussproofs/testbp2.pdf b/macros/latex/contrib/bussproofs/testbp2.pdf
new file mode 100644
index 0000000000..03a7f7a7a3
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/testbp2.pdf
Binary files differ
diff --git a/macros/latex/contrib/bussproofs/testbp2.tex b/macros/latex/contrib/bussproofs/testbp2.tex
new file mode 100644
index 0000000000..3dd30d98bd
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/testbp2.tex
@@ -0,0 +1,321 @@
+
+
+
+\documentclass[12pt]{article}
+\usepackage{bussproofs}
+\usepackage{amssymb}
+\usepackage{latexsym}
+
+% This is the "centered" symbol
+\def\fCenter{{\mbox{\Large$\rightarrow$}}}
+
+% Optional to turn on the short abbreviations
+\EnableBpAbbreviations
+
+% \alwaysRootAtTop % makes proofs upside down
+% \alwaysRootAtBottom % -- this is the default setting
+
+\begin{document}
+\thispagestyle{empty}
+
+When the {\tt bussproofs.sty} code was first written, the
+only documention for the {\tt bussproofs} style was in the
+comments at the beginning of the style file {\tt bussproofs.sty}.
+But recently (July 2004), Peter Smith has written an excellent
+exposition of {\tt bussproofs.sty}, presently available
+at
+\begin{center}
+\tt
+http://www.phil.cam.ac.uk/teaching\_staff/Smith/LaTeX/nd.html
+\end{center}
+
+The present document is
+a sample \LaTeX{} file that was created for testing
+purposes while writing the {\tt bussproofs} code and you might
+find that it useful as an example of how to
+use special features of the style.
+
+Author: Sam Buss \hspace*{1in} Email: {\tt sbuss@ucsd.edu}.
+\vspace*{0.25in}
+
+Here is some text.
+\begin{center}
+\Axiom$\Gamma^\prime\fCenter\Delta,A,A$
+\LeftLabel{Weakening}\RightLabel{}
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta, A$
+\LeftLabel{.}\RightLabel{\small $\lor$:right}
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\LeftLabel{eigenvariable $x$}\RightLabel{$\forall$:right}
+\UnaryInf$\Gamma \fCenter \Delta$
+\DisplayProof
+\end{center}
+Here is more text.
+\begin{prooftree}
+\alwaysDashedLine
+\alwaysDoubleLine
+\Axiom$\Delta\fCenter\Pi$
+\Axiom$\Gamma^\prime\fCenter\Delta,A$
+\dottedLine
+\singleLine
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\singleLine
+\UnaryInf$\Gamma \fCenter \Delta$
+\BinaryInf$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\Axiom$\fCenter\mbox{\rm Hi there}$
+\singleLine
+\BinaryInf$\Gamma\fCenter\Delta$
+\end{prooftree}
+\begin{center}
+\alwaysDoubleLine
+\AX$\Delta\fCenter\Pi$
+\AX$\Gamma^\prime\fCenter\Delta,A$
+\singleLine
+\UI$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UI$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\singleLine
+\UI$\Gamma \fCenter \Delta$
+\LL{.}\RightLabel{$\lor$:left}
+\BI$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\AXC{Hi there}
+\singleLine
+\BI$\Gamma\fCenter\Delta$
+\DisplayProof
+\end{center}
+The above examples show `displayed' proofs.
+On the other hand,
+for putting proofs inline instead of displayed,
+it is also permissable to put proofs into text rather than into
+centered environments. For example, one can write a proof right
+here:
+\centerAlignProof %Which ever one of these is LAST sets the vertical alignment
+\bottomAlignProof %Try commenting out all but one of these three lines.
+\normalAlignProof
+\Axiom$\Gamma^\prime\fCenter\Delta,A$
+\doubleLine
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\doubleLine
+\UnaryInf$\Gamma \fCenter \Delta$
+\Axiom$\Delta\fCenter\Pi$
+\kernHyps{-.5in}\insertBetweenHyps{\hskip-.25in}
+\BinaryInf$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\Axiom$\fCenter\mbox{\rm Hi there}$
+\doubleLine
+\BinaryInf$\Gamma\fCenter\Delta$
+\DisplayProof{} %% NOTE THE USE OF "{}"
+although of course the proof is quite big compared to the text.
+There is no reason you could not add \verb+\subscriptstyle+ or \verb+\small+
+commands to the lines of the proofs to shrink things down.
+The previous proof looks strange because it is illustrated the usage
+of \verb+\kernHyps+ and \verb+\insertBetweenHyps+. Finally
+a 3-ary inference with a usage of \verb+\noLine+ is:
+\begin{prooftree}
+\AxiomC{$A\lor B$}
+\AxiomC{$[A]$}
+\noLine
+\UnaryInfC{$C$}
+\AxiomC{$[B]$}
+\noLine
+\UnaryInfC{$C$}
+\TrinaryInfC{$C$}
+\end{prooftree}
+
+
+Two more examples:
+\begin{center}
+\AxiomC{A,B} \AxiomC{C} \BIC{A-B-C}
+\AXC{good} \AXC{bad} \BIC{$\frac{good}{bad}$A}
+\BIC{done}
+\DP
+\end{center}
+
+\begin{center}
+\Axiom$\fCenter A,B$ \Axiom$\fCenter C$ \BI$\fCenter A-B-C$
+\AX$\fCenter good$ \AX$\fCenter bad$ \BI$\fCenter\frac{good}{bad}A$
+\BI$\fCenter done$
+\DP
+\end{center}
+
+
+Small labels can be created as in the third proof below:
+\[
+\AxiomC{A}
+\RightLabel{1}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\RightLabel{(2)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\RightLabel{\scriptsize(3)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\LeftLabel{(4)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\]
+Arnold's example of inline proof: The figure
+\AxiomC{$\dots\Gamma_\iota\dots(\iota\in I)$}
+\RightLabel{$I$}
+\UnaryInfC{$\Gamma$}
+\DisplayProof{}
+is called ...
+%% NOTE THE USE OF "{}" after \DisplayProof to keep LaTeX from eating subsequent spaces!
+
+\bigskip
+
+\noindent{\bf Upside down proofs}
+Proofs can be rendered upside down. For instance the proof above with
+a 3-ary inference can be made upside down by giving the command
+\verb+\rootAtTop+. This is useful if you want your proof trees to have
+their root at the top.
+
+\alwaysRootAtTop % Henceforth puts the root at the top
+
+\begin{prooftree}
+\AxiomC{$A\lor B$}
+\AxiomC{$[A]$}
+\noLine
+\UnaryInfC{$C$}
+\AxiomC{$[B]$}
+\noLine
+\UnaryInfC{$C$}
+\TrinaryInfC{$C$}
+\end{prooftree}
+
+To make the change permanent for the rest of your document, use the
+command \verb+\alwaysRootAtTop+
+
+\bigskip
+
+\noindent
+Another upside-down example, from Alex Hertel:
+\bigskip
+
+\hbox{\kern-2cm%
+\tiny
+\rootAtTop
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (1 \wedge 1) \vee 0 ) \vee ( (0 \wedge 0) \vee 0 ) )$}
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (1 \wedge 1) \vee 1 ) \vee ( (0 \wedge 0) \vee 1 ) )$}
+\LeftLabel{$[0/z]$}
+\RightLabel{$[1/z]$}
+\BinaryInfC{$\forall z ( ( (1 \wedge 1) \vee z ) \vee ( (0 \wedge 0) \vee z ) )$}
+\RightLabel{$[0/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (1 \wedge \neg y) \vee z ) \vee ( (0 \wedge y) \vee z ) )$}
+\RightLabel{$[0/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (1 \wedge \neg y) \vee z ) \vee ( (0 \wedge y) \vee z ) )$}
+
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (0 \wedge 0) \vee 0 ) \vee ( (1 \wedge 1) \vee 0 ) )$}
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (0 \wedge 0) \vee 1 ) \vee ( (1 \wedge 1) \vee 1 ) )$}
+\LeftLabel{$[0/z]$}
+\RightLabel{$[1/z]$}
+\BinaryInfC{$\forall z ( ( (0 \wedge 0) \vee z ) \vee ( (1 \wedge 1) \vee z ) )$}
+\RightLabel{$[1/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (0 \wedge \neg y) \vee z ) \vee ( (1 \wedge y) \vee z ) )$}
+
+\LeftLabel{$[0/x]$}
+\RightLabel{$[1/x]$}
+\BinaryInfC{$\forall x \exists y \forall z ( ( (\neg x \wedge \neg y) \vee z ) \vee ( (x \wedge y) \vee z ) )$}
+\DisplayProof
+} % End of \hbox
+
+\bigskip
+
+
+\alwaysRootAtBottom
+Testing of quaternary and quinary inferences (a bit scrunched due a use of
+\verb+\insertBetweenHyps+):
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\AxiomC{$A^B$}
+\Axiom$A_B\fCenter A_{B_C}$
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuinaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuaternaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\end{prooftree}
+
+\alwaysRootAtTop
+Testing of quaternary and quinary inferences (a bit scrunched due a use of
+\verb+\insertBetweenHyps+):
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\AxiomC{$A^B$}
+\Axiom$A_B\fCenter A_{B_C}$
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuinaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuaternaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\end{prooftree}
+
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\TrinaryInf$X\fCenter XXXXX$
+\end{prooftree}
+
+\newenvironment{proof}{\begin{trivlist}\item[]{\bf Proof\ }}%
+{\end{trivlist}}
+\newenvironment{proofX}{\noindent{\bf Proof\ }}%
+{}
+
+\begin{proofX}
+\begin{prooftree}
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\BinaryInf$X\fCenter XXXXX$
+\end{prooftree}
+\end{proofX}
+
+\newbox\gnBoxA
+\newdimen\gnCornerHgt
+\setbox\gnBoxA=\hbox{$\ulcorner$}
+\global\gnCornerHgt=\ht\gnBoxA
+\newdimen\gnArgHgt
+
+\def\Godelnum #1{%
+ \setbox\gnBoxA=\hbox{$#1$}%
+ \gnArgHgt=\ht\gnBoxA%
+ \ifnum \gnArgHgt<\gnCornerHgt
+ \gnArgHgt=0pt%
+ \else
+ \advance \gnArgHgt by -\gnCornerHgt%
+ \fi
+ \raise\gnArgHgt\hbox{$\ulcorner$} \box\gnBoxA %
+ \raise\gnArgHgt\hbox{$\urcorner$}}
+
+This last sentence has nothing to do with proof trees, but shows my
+macros for G\"odel number delimeters:
+$\Godelnum A, \Godelnum B$
+$\Godelnum s$
+\end{document}