bussproofs-extra.dtx

% \iffalse meta-comment
%
%
% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
% ------------------------------------------------------
%
% 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/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
% 
% The Current Maintainer of this work is Richard Zach.
%
% This work consists of the files bussproofs-pextra.dtx,
% bussproofs-extra.ins, bussproofs-extra.sty
%
% \fi
%
% \iffalse
%<*driver>
\ProvidesFile{bussproofs-extra.dtx}
%</driver>
%<package>\NeedsTeXFormat{LaTeX2e}
%<package>\ProvidesPackage{bussproofs-extra}
%<package>   [2019/05/28 0.4 Extra commands for bussproofs.sty]
%<*driver>
\documentclass{ltxdoc}

\usepackage{bussproofs-extra}
\usepackage[colorlinks,allcolors=blue]{hyperref}
\usepackage{calc}

\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}}

\EnableCrossrefs         
\RecordChanges
\begin{document}
  \DocInput{bussproofs-extra.dtx}
  \PrintChanges
\end{document}
%</driver>
% \fi
%
% \CheckSum{0}
%
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
%
% \changes{v0.4}{2019/05/31}{Better implementation of line labels; add
% shortDeduce; style deduce lines} 
% \changes{v0.3}{2019/04/04}{Rename to bussproofs-extra.sty} 
% \changes{v0.2}{2014/10/16}{Fixed bug in dotsdDeduce, added examples}
% \changes{v0.1}{2014/04/26}{Initial version with deduce, linelabel functionality}
%
% \GetFileInfo{bussproofs-extra.sty}
%
% \DoNotIndex{\newcommand,\newenvironment}
%
%
% \title{The \textsf{bussproofs-extra} package\thanks{This document
%   corresponds to \textsf{bussproofs-extra}~\fileversion, dated \filedate.}}
% \author{\href{http://ucalgary.ca/rzach/}{Richard Zach}}
% \date{}
%
% \maketitle
%
% \section{Introduction}
%
% The \textsf{bussproofs-extra} package provides additional functionality for
% the proof tree typesetting package
% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\textsf{bussproofs}}
% by Sam Buss.  It is experimental and tested only with v.1.1, and
% only in \LaTeX{} mode with upward-growing trees.
% Functionality provided includes:
%
% \begin{enumerate}
% \item |\Deduce$| and |\DeduceC| commands, which work much
%  like |\Infer| commands but indicate missing parts of a proof.
% \item Multiple styles for typesetting the result of |\Deduce|,
% including 
% \begin{enumerate}
% \item |\straightDeduce|, which produces vertical dots
% \item |\branchDeduce|, which produces diagonal plus vertical dots
% \item |\ddotsDeduce|, which produces diagonal dots from top left
%  to bottom right
% \item |\dotsdDeduce|, which produces diagonal dots from top right
%  to bottom left
% \item |\shortDeduce|, which is like |\straightDeduce| but half the length
% \end{enumerate}
% |\straightDeduce| is the default.  It can be changed by redefining
% |\alwaysDeduce|.
% \item |\LeftLineLabel| and |\RightLineLabel| commands which
%   work like |\LeftLabel| and |\RightLabel| but place a label
%   next to the conclusion of an inference/deduction instead of the score
%   line.
% \item |\LeftSubproofLabel| and |\RightSubproofLabel| commands which
%   work like |\LeftLabel| and |\RightLabel| but place a label
%   next to the entire preceding subproof with a curly brace.
% \end{enumerate}
%
% Here's what these deductions look like:
%
% \begin{center}
% \begin{tabular}{@{}cccc@{}}
% \fbox{\AxiomC{$A$}
% \straightDeduce
% \DeduceC{$B$}
% \DisplayProof} &
% \fbox{\AxiomC{$A$}
% \branchDeduce
% \DeduceC{$B$}
% \DisplayProof} &
% \fbox{\AxiomC{$A$}
% \ddotsDeduce
% \DeduceC{$B$}
% \DisplayProof} &
% \fbox{\AxiomC{$A$}
% \dotsdDeduce
% \DeduceC{$B$}
% \DisplayProof} \\ \\
% \fbox{\Axiom$A \fCenter B$
% \straightDeduce
% \Deduce$A \lor C \fCenter B$
% \DisplayProof} &
% \fbox{\Axiom$A \fCenter B$
% \branchDeduce
% \Deduce$A \lor C \fCenter B$
% \DisplayProof} &
% \fbox{\Axiom$A  \fCenter B$
% \ddotsDeduce
% \Deduce$A \lor C \fCenter B$
% \DisplayProof} &
% \fbox{\Axiom$A \fCenter B$
% \dotsdDeduce
% \Deduce$A \lor C \fCenter B$
% \DisplayProof}
% \\ \\
% \texttt{straightDeduce} &
% \texttt{branchDeduce} &
% \texttt{ddotsDeduce} &
% \texttt{dotsdDeduce} 
% \end{tabular}
% \end{center}
%
%
% The most up-to-date version of this package is available at the
% \href{https://github.com/OpenLogicProject/bussproofs-extra}{Open Logic
% Project github site}, where you can file bug reports as well.
%
% \subsection{Example}
%
% \begin{verbatim}
% \begin{prooftree}
% \AxiomC{}
% \RightLabel{$\pi_1(a)$}
% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$
% \RightLabel{$\forall$R}
% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$
% \ddotsDeduce
% \RightLabel{$\pi_1'$}
% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$
% \AxiomC{}
% \RightLabel{$\pi_2$}
% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$
% \RightLabel{$\forall$L}
% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$
% \dotsdDeduce
% \RightLabel{$\pi_2'$}
% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$
% \RightLabel{cut}
% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$
% \RightLabel{$\pi_4$}
% \branchDeduce
% \Deduce$\Pi \fCenter \Xi$
% \end{prooftree}
% \end{verbatim}
% produces this:
% \begin{prooftree}
% \AxiomC{}
% \RightLabel{$\pi_1(a)$}
% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$
% \RightLabel{$\forall$R}
% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$
% \ddotsDeduce
% \RightLabel{$\pi_1'$}
% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$
% \AxiomC{}
% \RightLabel{$\pi_2$}
% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$
% \RightLabel{$\forall$L}
% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$
% \dotsdDeduce
% \RightLabel{$\pi_2'$}
% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$
% \RightLabel{cut}
% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$
% \RightLabel{$\pi_4$}
% \branchDeduce
% \Deduce$\Pi \fCenter \Xi$
% \end{prooftree}

% It is also possible to label entire subproofs on the left and on the right.
% \begin{verbatim}
% \begin{prooftree}
% \AxiomC{}
% \Deduce$\Gamma \fCenter \Delta$
% \LeftLineLabel{$S_1$}
% \Deduce$\Gamma \fCenter \Delta, A$
% \LeftSubproofLabel{$\pi$}
% \AxiomC{}
% \Deduce$\Gamma' \fCenter \Delta'$
% \LeftLineLabel{$S_2$}
% \Deduce$A, \Gamma' \fCenter \Delta'$
% \RightSubproofLabel{$\pi'$}
% \RightLabel{cut}
% \LeftLineLabel{$S_3$}
% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$
% \Deduce$\Pi \fCenter \Lambda$
% \end{prooftree}
% \end{verbatim}
% \begin{prooftree}
% \AxiomC{}
% \Deduce$\Gamma \fCenter \Delta$
% \Deduce$\Gamma \fCenter \Delta, A$
% \LeftSubproofLabel{$\pi$}
% \AxiomC{}
% \Deduce$\Gamma' \fCenter \Delta'$
% \Deduce$A, \Gamma' \fCenter \Delta'$
% \RightSubproofLabel{$\pi'$}
% \RightLabel{cut}
% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$
% \Deduce$\Pi \fCenter \Lambda$
% \end{prooftree}
%
% The |\LeftLineLabel| and |\RightLineLabel| commands add labels to
% the sequent or formula produced by the following |\Axiom|, |\XxxxInf|,
% and |\Deduce| command. 
% \begin{prooftree}
%    \LeftLineLabel{$S_1$}
%    \RightLineLabel{$S_1$}
%    \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$
%    \LeftLineLabel{$S_2$}
%    \RightLineLabel{$S_2$}
%    \UnaryInf$A, \Gamma \fCenter \Delta, B$
%    \LeftLineLabel{$S_3$}
%    \Deduce$\Pi \fCenter \Lambda$
%    \LeftLineLabel{$S_1'$}
%    \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}}
%    \LeftLineLabel{$S_2'$}
%    \UnaryInfC{$A \lor B$}
%    \LeftLineLabel{$S_3'$}
%    \DeduceC{$C$}
%    \LeftLineLabel{$S_4$}
%    \BinaryInf$\Pi \fCenter \Lambda$
%    \RightLineLabel{$S_5$}
%    \UnaryInf$\Pi \fCenter \Lambda$
% \end{prooftree}
% If the sequent or formula is itself a premise of an |\XxxInf|
% command and the conclusion is longer, this may produce a less 
% than optimal result, as the label is produced before the score 
% line below (compare the left and right labels of the top left
% sequent above). In that case you may want to insert extra space 
% using |\phantom|, or use |\makebox| and the |\widthof| command 
% of the |calc| package for the |XxxC| variants of the commands 
% (see the top right formula below) as in the |\Axiom| commands 
% below.
% \begin{verbatim}  
% \begin{prooftree}
%    \LeftLineLabel{$S_1$}
%    \RightLineLabel{$S_1$}
%    \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$
%    \LeftLineLabel{$S_2$}
%    \RightLineLabel{$S_2$}
%    \UnaryInf$A, \Gamma \fCenter \Delta, B$
%    \LeftLineLabel{$S_3$}
%    \Deduce$\Pi \fCenter \Lambda$
%    \LeftLineLabel{$S_1'$}
%    \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}}
%    \LeftLineLabel{$S_2'$}
%    \UnaryInfC{$A \lor B$}
%    \LeftLineLabel{$S_3'$}
%    \DeduceC{$C$}
%    \LeftLineLabel{$S_4$}
%    \BinaryInf$\Pi \fCenter \Lambda$
%    \RightLineLabel{$S_5$}
%    \UnaryInf$\Pi \fCenter \Lambda$
% \end{prooftree}    
% \end{verbatim}    
%
% \StopEventually{}
%
% \section{Implementation}
%
% \subsection{Setup}
% 
% We require \textsf{bussproofs} (obviously) and and \textsf{tikz} for
% drawing things.
%
%    \begin{macrocode}
\RequirePackage{bussproofs}
\RequirePackage{tikz}
%    \end{macrocode}
% \subsection{Dimensions and boxes}
% 
% \textsf{bussproofs} aligns sequents at the right end of the sequent
% arrow, so we need to remember by how much to correct to get
% deductions to the middle of sequents.  For |\ddotsDeduce| and
% |\dotsdDeduce| (diagonal) styles, the upper and lower sequents will be
% displaced.
%    \begin{macrocode}
\newdimen\CenterCorrection
\newdimen\DiagCorrection
%    \end{macrocode}
% We need two boxes to hold the left and right line labels.
%    \begin{macrocode}
\newbox\myBoxLLL
\newbox\myBoxRLL
%    \end{macrocode} 
% \subsection{Deduce Styles} 
%
% The following commands set the style for the next |\Deduce|
% command. |\straightDeduce| produces a simple vertical line of dots,
% and |\shortDeduce| a line of half that length.
% |\branchDeduce| produces centered branching (Takeuti/Gentzen-style)
% dots, |\ddotsDeduce| left-to-right diagonal dots, and |\dotsdDeduce|
% right-to-left diagonal dots. They do this by redefining the
% |\fDeduce| command which produces the dots and sets up the
% dimensions. The TikZ style |deduceLine| is used as argument to the
% |\draw| command and can be redefined for other line styles as well
% (e.g., smaller dots or closer spacing).
%    \begin{macrocode}
\tikzset{
    deduceLine/.style = {line width=1.1pt, loosely dotted}}

\def\straightDeduce{%
  \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,1);}
  \global\DiagCorrection=0pt
  \ignorespaces
}

\def\shortDeduce{%
  \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,.5);}
  \global\DiagCorrection=0pt
  \ignorespaces
}

\def\branchDeduce{%
  \gdef\fDeduce{\begin{tikzpicture}
      \draw[deduceLine] (0,0) -- (0,1);
      \draw[deduceLine] (-.5,.5) -- (0,0);
      \draw[deduceLine] (.5,.5) -- (0,0);
  \end{tikzpicture}}
  \global\DiagCorrection=0pt
  \ignorespaces
}

\def\ddotsDeduce{%
  \gdef\fDeduce{\begin{tikzpicture}
      \draw[deduceLine] (0,1) -- (1,0);
  \end{tikzpicture}}
  \setbox\myBoxA=\hbox{\fDeduce}
  \global\DiagCorrection=-\wd\myBoxA
  \ignorespaces
}

\def\dotsdDeduce{%
  \gdef\fDeduce{\begin{tikzpicture}
      \draw[deduceLine] (1,1) -- (0,0);
  \end{tikzpicture}}
  \setbox\myBoxA=\hbox{\fDeduce}
  \global\DiagCorrection=\wd\myBoxA
  \ignorespaces
}
%    \end{macrocode}
% The |\alwaysDeduce| command is used to (re)set the
% deduce style to a default and is executed every time a deduction is
% typeset. It can be redefined to change the default deduce style.
%    \begin{macrocode}
\def\alwaysDeduce{\straightDeduce}
\straightDeduce
%    \end{macrocode}
% \subsection{\texttt{\textbackslash Deduce\$} and
% \texttt{\textbackslash DeduceC}}
% 
% |\Deduce$| and |\DeduceC| are the commands to actually produce the
% deductions. They are used and work just like |\UnaryInf$| and
% |\UnaryInfC|.
%    \begin{macrocode}
\def\Deduce$#1\fCenter#2${%
    \prepUnary%
    \buildConclusion{#1}{#2}%
    \setbox\myBoxA=\hbox{\fCenter}%
    \global\CenterCorrection=-.5\wd\myBoxA
    \joinDeduce%
    \resetInferenceDefaults%
    \ignorespaces%
}

\def\DeduceC#1{
    \prepUnary%
    \buildConclusionC{#1}%
    \global\CenterCorrection=0pt
    \joinDeduce%
    \resetInferenceDefaults%
    \ignorespaces%
}
%    \end{macrocode}
% \section{Typesetting the Deduction}
% 
% |\joinDeduce| aligns and joins |\curBox| and |\myBoxC| into a single
% |vbox|.  |\curBox| holds the upper proof, |\curScoreStart| is
% distance to where the line below the premise would start,
% |\curScoreCenter| is distance from left edge of score to the 
% alignment point, and |\curScoreEnd| is width of the score line.
%    \begin{macrocode}

\def\joinDeduce{%
    \global\advance\curCenter by -\hypKernAmt%
%    \end{macrocode}
% If center of premise is left of center of conclusion move upper box
% to right by difference, else move lower box right by difference
%    \begin{macrocode}
    \ifnum\curCenter<\newCenter%
        \displace=\newCenter%
        \advance \displace by -\curCenter%
        \kernUpperBox%
    \else% 
        \displace=\curCenter%
        \advance \displace by -\newCenter%
        \kernLowerBox%
    \fi%
%    \end{macrocode}
% For |\ddotsDeduce|, move lower box right; for |\dotsdDeduce|, move
% upper box right; then set |\curCenter| to align with horizontal center
% of dots.
%    \begin{macrocode}
    \ifnum\DiagCorrection<0%
        \displace=-\DiagCorrection
        \kernLowerBox%
    \else
        \displace=\DiagCorrection
        \kernUpperBox%
    \fi%
    \advance\curCenter by-.5\DiagCorrection
%    \end{macrocode}
% Now we draw the deduction.
%    \begin{macrocode}
    \buildDeduce%
%    \end{macrocode}
% Put the deduction and labels into a box.
%    \begin{macrocode}
    \buildScoreLabels%
%    \end{macrocode}
% Put everything into a new box and compute the dimensions for the
% next |\Deduce| or |\XxxxInf|.
%    \begin{macrocode}
    \ifx\rootAtBottomFlag\myTrue%
        \buildRootBottom%
    \else%
        \buildRootTop%
    \fi%
    \global \curScoreStart=\newScoreStart%
    \global \curScoreEnd=\newScoreEnd%
    \global \curCenter=\newCenter%
}
%    \end{macrocode}
% |\buildDeduce| does for |\DeduceX| what |\buildInf| does for
% |\XxxInf|: put the deduction bit (dots) into a box and set the
% dimensions properly.
%    \begin{macrocode}

\def\buildDeduce{%
    \global\setbox \myBoxD =%
        \hbox{\fDeduce}%
    \displace = \wd\myBoxD % find width of vdots
%    \end{macrocode}
% set start and end of current score to left and right of the box
% holding the deduction.
%    \begin{macrocode}
    \global\curScoreStart = \curCenter% 
    \global\advance\curScoreStart by -.5\displace%
    \global\curScoreEnd = \curCenter% 
    \global\advance\curScoreEnd by .5\displace%
    \global\advance\curScoreStart by\CenterCorrection
    \global\advance\curScoreEnd by\CenterCorrection
}
%    \end{macrocode}
% \subsection{Line Labels}
% 
% |\LeftLineLabel| and |\RightLineLabel| set the label to place to the
% left or right, respectively, of the conclusion of the next |\Axiom|,
% |\XxxInf| or |\Deduce| command. They are aligned with the text
% produced by |\LeftLabel| and |\RightLabel| (i.e., the distance to
% the line is $|\ScoreOverhang| + |\labelSpacing|$.
%    \begin{macrocode}

\def\LeftLineLabel#1{%
  \global\def\displayLeftLineLabel{%
    {#1\hskip\labelSpacing}}
  \ignorespaces}

\def\RightLineLabel#1{%
  \global\def\displayRightLineLabel{%
    {\hskip\labelSpacing #1}}
  \ignorespaces}

\global\let\displayLeftLineLabel\relax
\global\let\displayRightLineLabel\relax
%    \end{macrocode}
%
% \subsection{Subproof Labels}
% Sometimes you'd like to lable entire subproofs.  This is done with
% commands |\LeftSubproofLabel| and |\RightSubproofLabel|.
%    \begin{macrocode}

\def\LeftSubproofLabel#1{%
  \global\setbox\curBox =
  \hbox{\vbox to \ht\curBox{%
      \vfil
      \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}%
      \vfil}\box\curBox}%
}

\def\RightSubproofLabel#1{%
  \displace=\ht\curBox
  \global\setbox\curBox =
  \hbox{\box\curBox\vbox to \displace{%
      \vfil
      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}%
      \vfil}}%
}
%    \end{macrocode}
% \subsection{Patched commands from \textsf{bussproofs}}
%
% Some commands from \textsf{bussproofs.sty} have to be redefined to include
% |bussproofs-extra| functionality. Added/changed lines are indicated by a
% |%bpextra| comment
%    \begin{macrocode}
\def\resetInferenceDefaults{%
    \global\def\theHypSeparation{\defaultHypSeparation}%
    \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
    \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
    \global\def\buildScore{\alwaysBuildScore}%
    \global\def\theScoreFiller{\alwaysScoreFiller}%
    % reset line labels to nothing %bpextra
    \global\let\displayLeftLineLabel\relax %bpextra
    \global\let\displayRightLineLabel\relax %bpextra
    % reset to defaul deduce style %bpextra
    \alwaysDeduce %bpextra
    \gdef\hypKernAmt{0pt}% Restore to zero kerning.
}

\def\Axiom$#1\fCenter#2${%
    % Get level and correct names set.
    \prepAxiom%
    % Define the boxes
    % bpextra -- add line labels
    \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% 
    \setbox\myBoxB=\hbox{$#2$}% %bpextra
    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
    \global\setbox\curBox=%
         \hbox{\unhcopy\myBoxLLL%bpextra
         \hskip\ScoreOverhangLeft\relax
         \unhcopy\myBoxA
         \unhcopy\myBoxB
         \hskip\ScoreOverhangRight
         \unhcopy\myBoxRLL}%bpextra
    % Set the relevant dimensions for the boxes
    \global\curScoreStart=0pt \relax
    \global\curScoreEnd=\wd\curBox \relax
    \global\curCenter=\wd\myBoxA \relax %bpextra
    \global\advance \curCenter by \ScoreOverhangLeft%
    % bpextra adjust by dimensions of labels
    \global\advance \curCenter by \wd\myBoxLLL%bpextra
    \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
    \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
    % reset line labels to nothing %bpextra
    \global\let\displayLeftLineLabel\relax %bpextra
    \global\let\displayRightLineLabel\relax %bpextra
    \ignorespaces
}

\def\AxiomC#1{      % Note argument not in math mode
    % Get level and correct names set.
    \prepAxiom%
        % Define the box.
    \setbox\myBoxA=\hbox{#1}%
    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
    \global\setbox\curBox =%
        \hbox{\unhcopy\myBoxLLL%bpextra
            \hskip\ScoreOverhangLeft\relax%
            \unhcopy\myBoxA
            \hskip\ScoreOverhangRight\relax
            \unhcopy\myBoxRLL}% %bpextra
    % Set the relevant dimensions for the boxes
        \global\curScoreStart=0pt \relax
        \global\curScoreEnd=\wd\curBox \relax
        \global\curCenter=.5\wd\myBoxA \relax %bpextra
        \global\advance \curCenter by \ScoreOverhangLeft%
    % bpextra adjust by dimensions of labels
    \global\advance \curCenter by \wd\myBoxLLL%bpextra
    \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
    \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
    % reset line labels to nothing %bpextra
    \global\let\displayLeftLineLabel\relax %bpextra
    \global\let\displayRightLineLabel\relax %bpextra
    \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$}% 
        \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
        \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
    % Put them together in \myBoxC
    \setbox\myBoxC =%
          \hbox{\unhcopy\myBoxLLL%bpextra
          \hskip\ScoreOverhangLeft\relax%
        \unhcopy\myBoxA\unhcopy\myBoxB
        \hskip\ScoreOverhangRight
        \unhcopy\myBoxRLL}% %bpextra
    % Calculate the center of the \myBoxC string.
    \newScoreStart=0pt \relax%
    \newCenter=\wd\myBoxA \relax%
    \advance \newCenter by \ScoreOverhangLeft%
    \newScoreEnd=\wd\myBoxC%
    % bpextra adjust by dimensions of labels
    \global\advance\newCenter by \wd\myBoxLLL%bpextra
    \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
    \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
    % reset line labels to nothing %bpextra
    \global\let\displayLeftLineLabel\relax %bpextra
    \global\let\displayRightLineLabel\relax %bpextra
}

\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
        % Define the box.
    \setbox\myBoxA=\hbox{#1}%
    \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
    \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
\setbox\myBoxC =%
        \hbox{\unhcopy\myBoxLLL%bpextra
            \hskip\ScoreOverhangLeft\relax%
            \unhcopy\myBoxA
            \hskip\ScoreOverhangRight
            \unhcopy\myBoxRLL}%bpextra
    % Calculate kerning to line up centers
    \newScoreStart=0pt \relax%
    \newCenter=.5\wd\myBoxA \relax% bpextra
    \newScoreEnd=\wd\myBoxC%
        \advance \newCenter by \ScoreOverhangLeft%
    % bpextra adjust by dimensions of labels
    \global\advance\newCenter by \wd\myBoxLLL%bpextra
    \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
    \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
    % reset line labels to nothing %bpextra
    \global\let\displayLeftLineLabel\relax %bpextra
    \global\let\displayRightLineLabel\relax %bpextra
}
%    \end{macrocode}
% \Finale
% \PrintChanges
\endinput