bussproofs-extra (4apr19)

git-svn-id: svn://tug.org/texlive/trunk@50760 c570f23f-e606-0410-a88d-b1316a301751

12 files changed, 952 insertions, 2 deletions

diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/README.md b/Master/texmf-dist/doc/latex/bussproofs-extra/README.md
new file mode 100644
index 00000000000..2b8ed7088ce
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/bussproofs-extra/README.md
@@ -0,0 +1,19 @@
+bussproofs-extra
+================
+
+Additional functionality for bussproofs.sty. Specifically, it allows
+for typesetting of entire (sub)deductions.
+
+To install, download the files, and run 
+```
+latex bussproofs-extra.ins
+```
+To generate the documentation, run
+```
+pdflatex bussproofs-extra.dtx
+makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo 
+pdflatex bussproofs-extra.dtx
+pdflatex bussproofs-extra.dtx
+```
+
+This package is distributed under the terms of the LPPL 1.3c
diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty b/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty
new file mode 100644
index 00000000000..e83935d50d6
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty
@@ -0,0 +1,5 @@
+% Wrapper for backwards compatibility
+
+\RequirePackage{bussproofs-extra}
+\PackageWarning{bussproofs-extra}{You've loaded bussproofs with
+  bpextra, but you should use bussproofs-extra instead}
diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf b/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf
new file mode 100644
index 00000000000..9075a6a8cc2
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf
diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/Makefile b/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
new file mode 100644
index 00000000000..3285cb49a3f
--- /dev/null
+++ b/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
@@ -0,0 +1,10 @@
+ALL: bussproofs-extra.sty bussproofs-extra.pdf
+
+bussproofs-extra.sty: bussproofs-extra.dtx bussproofs-extra.ins
+	latex bussproofs-extra.ins
+
+bussproofs-extra.pdf: bussproofs-extra.sty
+	pdflatex bussproofs-extra.dtx
+	makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo
+	pdflatex bussproofs-extra.dtx
+	pdflatex bussproofs-extra.dtx
diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
new file mode 100644
index 00000000000..59cc56e7503
--- /dev/null
+++ b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
@@ -0,0 +1,592 @@
+% \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/04/04 0.3 Extra commands for bussproofs.sty]
+%<*driver>
+\documentclass{ltxdoc}
+
+<<<<<<< HEAD:bussproofs-extra.dtx
+\usepackage{bussproofs-extra}
+\usepackage[colorlinks]{hyperref}
+=======
+\usepackage{bpextra}
+\usepackage[colorlinks,allcolors=blue]{hyperref}
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+
+\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}}
+
+\EnableCrossrefs         
+\CodelineIndex
+\RecordChanges
+\begin{document}
+  \DocInput{bussproofs-extra.dtx}
+  \PrintChanges
+  \PrintIndex
+\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.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
+% \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 intead of the score
+%   line.  \textbf{These don't work properly and may be removed!}
+% \end{enumerate}
+%
+% Here's what these deductions look like:
+%
+% \begin{center}
+% \begin{tabular}{@{}llll@{}}
+% \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$
+% \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}
+% \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}
+
+
+%
+% \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}
+% 
+% \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} 
+% \subsection{Deduce Styles} 
+%
+% The following commands set the style for the next |\Deduce|
+% command. |\straightDeduce| produces a simple vertical line of dots,
+% |\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 |\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\straightDeduce{%
+  \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\branchDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,0) -- (0,1);
+      \draw[very thick,loosely dotted] (-.5,.5) -- (0,0);
+      \draw[very thick,loosely dotted] (.5,.5) -- (0,0);
+  \end{tikzpicture}}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\ddotsDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,1) -- (1,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=-\wd\myBoxA
+  \ignorespaces
+}
+
+\def\dotsdDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (1,1) -- (0,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=\wd\myBoxA
+  \ignorespaces
+}
+
+\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}
+    % if we align at \fCenter, move \fDeduce left by 1/2 width of \fCenter 
+    \global\CenterCorrection=-.5\wd\myBoxA
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\DeduceC#1{
+    \prepUnary%
+    \buildConclusionC{#1}%
+    % vdot alignment is off by a bit, correct
+    \global\CenterCorrection=-4pt
+    % Align and join the curBox and the new box into one vbox.
+    \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
+    %\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%
+%    \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{%
+    \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}}
+  \ignorespaces}
+
+\def\RightLineLabel#1{%
+  \global\def\displayRightLineLabel{
+    \rlap{\hskip\ScoreOverhangLeft\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 =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\vbox to \ht\curBox{\vfil\llap{#1
+        $\left\{\vrule height .5\ht\curBox width 0pt\right.$}\vfil}\box\curBox}%
+=======
+  \hbox{\vbox to \ht\curBox{%
+      \vfil
+      \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}%
+      \vfil}\box\curBox}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+\def\RightSubproofLabel#1{%
+  \displace=\ht\curBox
+  \global\setbox\curBox =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\box\curBox\vbox to \displace{\vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}\vfil}}%
+=======
+  \hbox{\box\curBox\vbox to \displace{%
+      \vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}
+      \vfil}}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+%    \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{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+    \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    \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{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \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\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
+    % Define the boxes
+        \setbox\myBoxA=\hbox{\displayLeftLineLabel $\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+        \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    % 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{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \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%
+}
+%    \end{macrocode}
+% \Finale
+% \PrintChanges
+\endinput
diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins
new file mode 100644
index 00000000000..e511feff730
--- /dev/null
+++ b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins
@@ -0,0 +1,57 @@
+%%
+%% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+%%
+%% This file may be distributed and/or modified under the conditions of
+%% the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version
+%% 1999/12/01 or later.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/bussproofs-extra}
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+
+This file 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
+1999/12/01 or later.
+
+\endpreamble
+
+\generate{\file{bussproofs-extra.sty}{\from{bussproofs-extra.dtx}{package}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{*                                                           *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX:                    *}
+\Msg{*                                                           *}
+\Msg{*     bussproofs-extra.sty                                  *}
+\Msg{*                                                           *}
+\Msg{* To produce the documentation run the file bpextra.dtx     *}
+\Msg{* through LaTeX, and then                                   *}
+\Msg{* makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo *}
+\Msg{* Then run LaTeX on bussproofs-extra.dtx again              *}
+\Msg{*                                                           *}
+\Msg{* Happy TeXing!                                             *}
+\Msg{*                                                           *}
+\Msg{*************************************************************}
+
+\endbatchfile
diff --git a/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
new file mode 100644
index 00000000000..e740e1ef218
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
@@ -0,0 +1,265 @@
+%%
+%% This is file `bussproofs-extra.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% bussproofs-extra.dtx  (with options: `package')
+%% 
+%% This is a generated file.
+%% 
+%% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+%% 
+%% This file 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
+%% 1999/12/01 or later.
+%% 
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{bussproofs-extra}
+   [2019/04/04 0.3 Extra commands for bussproofs.sty]
+
+
+\RequirePackage{bussproofs}
+\RequirePackage{tikz}
+
+\newdimen\CenterCorrection
+\newdimen\DiagCorrection
+
+\def\straightDeduce{%
+  \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\branchDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,0) -- (0,1);
+      \draw[very thick,loosely dotted] (-.5,.5) -- (0,0);
+      \draw[very thick,loosely dotted] (.5,.5) -- (0,0);
+  \end{tikzpicture}}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\ddotsDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,1) -- (1,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=-\wd\myBoxA
+  \ignorespaces
+}
+
+\def\dotsdDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (1,1) -- (0,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=\wd\myBoxA
+  \ignorespaces
+}
+
+\def\alwaysDeduce{\straightDeduce}
+\straightDeduce
+
+\def\Deduce$#1\fCenter#2${%
+    \prepUnary%
+    \buildConclusion{#1}{#2}%
+    \setbox\myBoxA=\hbox{\fCenter}
+    % if we align at \fCenter, move \fDeduce left by 1/2 width of \fCenter
+    \global\CenterCorrection=-.5\wd\myBoxA
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\DeduceC#1{
+    \prepUnary%
+    \buildConclusionC{#1}%
+    % vdot alignment is off by a bit, correct
+    \global\CenterCorrection=-4pt
+    % Align and join the curBox and the new box into one vbox.
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\joinDeduce{%
+    \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\DiagCorrection<0%
+        \displace=-\DiagCorrection
+        \kernLowerBox%
+    \else
+        \displace=\DiagCorrection
+        \kernUpperBox%
+    \fi%
+    \advance\curCenter by-.5\DiagCorrection
+    %\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%
+    \buildDeduce%
+    \buildScoreLabels%
+    \ifx\rootAtBottomFlag\myTrue%
+        \buildRootBottom%
+    \else%
+        \buildRootTop%
+    \fi%
+    \global \curScoreStart=\newScoreStart%
+    \global \curScoreEnd=\newScoreEnd%
+    \global \curCenter=\newCenter%
+}
+
+\def\buildDeduce{%
+    \global\setbox \myBoxD =%
+        \hbox{\fDeduce}%
+    \displace = \wd\myBoxD % find width of vdots
+    \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
+}
+
+\def\LeftLineLabel#1{%
+  \global\def\displayLeftLineLabel{%
+    \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}}
+  \ignorespaces}
+
+\def\RightLineLabel#1{%
+  \global\def\displayRightLineLabel{
+    \rlap{\hskip\ScoreOverhangLeft\hskip\labelSpacing #1}}
+  \ignorespaces}
+
+\global\let\displayLeftLineLabel\relax
+\global\let\displayRightLineLabel\relax
+
+
+\def\LeftSubproofLabel#1{%
+  \global\setbox\curBox =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\vbox to \ht\curBox{\vfil\llap{#1
+        $\left\{\vrule height .5\ht\curBox width 0pt\right.$}\vfil}\box\curBox}%
+=======
+  \hbox{\vbox to \ht\curBox{%
+      \vfil
+      \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}%
+      \vfil}\box\curBox}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+\def\RightSubproofLabel#1{%
+  \displace=\ht\curBox
+  \global\setbox\curBox =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\box\curBox\vbox to \displace{\vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}\vfil}}%
+=======
+  \hbox{\box\curBox\vbox to \displace{%
+      \vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}
+      \vfil}}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+\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{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+    \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    \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{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \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\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
+    % Define the boxes
+        \setbox\myBoxA=\hbox{\displayLeftLineLabel $\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+        \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    % 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{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \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%
+}
+\endinput
+%%
+%% End of file `bussproofs-extra.sty'.
diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check
index 79eafd062a4..836581a51d6 100755
--- a/Master/tlpkg/bin/tlpkg-ctan-check
+++ b/Master/tlpkg/bin/tlpkg-ctan-check
@@ -128,7 +128,7 @@ my @TLP_working = qw(
     br-lex bracketkey braids braille braket
     brandeis-dissertation brandeis-problemset
     breakcites breakurl bredzenie breqn bropd brushscr
-    bullcntr bundledoc burmese businesscard-qrcode bussproofs
+    bullcntr bundledoc burmese businesscard-qrcode bussproofs bussproofs-extra
     bxbase bxcalc bxcjkjatype bxdpx-beamer bxdvidriver
     bxjaholiday bxjaprnind bxpapersize bxpdfver bxeepic bxenclose
     bxjalipsum bxjscls bxnewfont bxorigcapt bxtexlogo bxwareki bytefield 
diff --git a/Master/tlpkg/libexec/ctan2tds b/Master/tlpkg/libexec/ctan2tds
index d8bad3cc209..1ce7d296eee 100755
--- a/Master/tlpkg/libexec/ctan2tds
+++ b/Master/tlpkg/libexec/ctan2tds
@@ -1663,6 +1663,7 @@ $standardtex
  'blockdraw_mp','NULL',                 # skip .sty's
  'booktabs-de', 'NULL',                 # doc package
  'booktabs-fr', 'NULL',                 # doc package
+ 'bussproofs-extra', 'bussproofs-extra.sty',		# not bpextra.sty
  'breqn',       '\.sty|\.sym',
  'c-pascal',    '^[^d].*\.tex|' . $standardtex, # not demo*.tex
  'calxxxx',     'cal.*\.tex',
diff --git a/Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc b/Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc
new file mode 100644
index 00000000000..e69de29bb2d
--- /dev/null
+++ b/Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc
diff --git a/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc
index 93457572451..d31e83ed24f 100644
--- a/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc
+++ b/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc
@@ -110,7 +110,6 @@ depend bracketkey
 depend braket
 depend breakurl
 depend bullcntr
-depend bussproofs
 depend bxcalc
 depend bxdpx-beamer
 depend bxdvidriver
diff --git a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
index f9abeffdd81..cbf9c645cbb 100644
--- a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
+++ b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
@@ -27,6 +27,8 @@ depend boldtensors
 depend bosisio
 depend bpchem
 depend bropd
+depend bussproofs
+depend bussproofs-extra
 depend bytefield
 depend calculation
 depend cascade