summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/bussproofs
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2006-10-12 20:18:11 +0000
committerKarl Berry <karl@freefriends.org>2006-10-12 20:18:11 +0000
commit300275364d8fd9b6da6085545073c87d08d94f32 (patch)
treeb9e5fbe5294d236a426be9f0bf878398d5ff87cd /Master/texmf-dist/tex/latex/bussproofs
parent1c1a6fed5bb196c6dc3231b3de9e59b02784252f (diff)
new package bussproofs (12oct06)
git-svn-id: svn://tug.org/texlive/trunk@2323 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/bussproofs')
-rw-r--r--Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty909
1 files changed, 909 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
new file mode 100644
index 00000000000..b5d7cc83bd5
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
@@ -0,0 +1,909 @@
+%
+\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.0.}
+% bussproofs.sty. Version 1.0
+% (c) 1994,1995,1996,2004,2005,2006. Copyright retained by Samuel R. Buss.
+% 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.
+% 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.
+
+% A good exposition of how to use bussproofs.sty (version 0.9) has been written
+% by Peter Smith and is available on the internet.
+% 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 letter commands are enabled. This allows
+% \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.
+% 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 \(...\) ).
+%
+% \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>}
+%
+% \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\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 DONT 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}
+%\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\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\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\box\myBoxA\lower\htCbox\box\ccurBox%
+ \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\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
+}
+