summaryrefslogtreecommitdiff
path: root/macros/generic/proofs
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/generic/proofs
Initial commit
Diffstat (limited to 'macros/generic/proofs')
-rw-r--r--macros/generic/proofs/taylor/QED.sty731
-rw-r--r--macros/generic/proofs/taylor/prooftree-doc.dvibin0 -> 7336 bytes
-rw-r--r--macros/generic/proofs/taylor/prooftree-doc.pdfbin0 -> 80732 bytes
-rw-r--r--macros/generic/proofs/taylor/prooftree-doc.tex198
l---------macros/generic/proofs/taylor/prooftree.sty1
-rw-r--r--macros/generic/proofs/taylor/prooftree.tex347
6 files changed, 1277 insertions, 0 deletions
diff --git a/macros/generic/proofs/taylor/QED.sty b/macros/generic/proofs/taylor/QED.sty
new file mode 100644
index 0000000000..bdf443cee1
--- /dev/null
+++ b/macros/generic/proofs/taylor/QED.sty
@@ -0,0 +1,731 @@
+\message{<Paul Taylor's right-justified end-of-proof mark, 24 June 1995>}
+%%========================================================================
+%************************************************************************%
+%* *%
+%* Maybe you already have a \qed macro to put a little square *%
+%* on the right hand side at the end of a mathematical proof? *%
+%* *%
+%* IT'S PROBABLY MINE! *%
+%* *%
+%* Please compare yours with \parag@pushright below. *%
+%* *%
+%* This new file is compatible, it fixes the bugs, has extra *%
+%* features, and is maintained and portable. Please use it! *%
+%* *%
+%* NEW FEATURE \WillHandleQED and \HandleQED for environments *%
+%* which do not give access to the right hand side of the page. *%
+%* *%
+%* Now also available: \DefineStandardTheorems or *%
+%* \usepackage[define-standard-theorems]{QED} *%
+%* *%
+%************************************************************************%
+%========================================================================%
+
+% COPYRIGHT (C) 1993-6 Paul Taylor, Department of Computer Science,
+% Queen Mary & Westfield College, London E1 4NS.
+% You may use this file for any purpose. You may copy it on condition that
+% you do so in exactly the form in which it was supplied, make no charge
+% for the copy and impose the same conditions on the recipient.
+% This software is supplied ``as is'' without warranty, express or implied,
+% including but not limited to merchantability and fitness for any particular
+% purpose. No liability is accepted by the author, Queen Mary and Westfield
+% College, Imperial College or any third party for any direct or consequential
+% damages, however caused.
+% In all cases you must keep several backup versions of your files in a place
+% to which your machine cannot write, and you must check documents visually
+% before submitting the final version to a publisher or expensive printer.
+
+% WARNING: If you use this with Frank Mittlebach's "theorem.sty" you
+% MUST load theorem first, then QED, then do the \newtheorem commands.
+
+% Authoritative version: /pub/tex/contrib/pt/proofs/QED.sty
+% by anonymous FTP from: ftp.dcs.qmw.ac.uk
+% also CTAN: macros/generic/proofs/taylor/QED.sty
+% author/maintained by: Dr Paul Taylor <pt@dcs.qmw.ac.uk>
+
+% WARNING: This file replaces some of the functions of "Paul.sty"
+% and MUST NOT be used with it as serious conflicts will arise.
+
+%=========================================================================
+
+% USER INTERFACE AND EXAMPLES (see also OPTIONS below)
+
+% LaTeX2e \usepackage options: see \DeclareOption commands below
+% theorems-as-commands roman-theorems italic-theorems
+% auto-QED explicit-QED number-theorems dont-number-theorems
+% black-square open-square
+
+% \begin{Proof} ... \end{Proof}
+% or \Proof ... \endProof
+% or \Proof ... \endproof
+% or \Proof ... \qed also \QED \QEF and \QEI
+
+% WARNING: \qed which doesn't follow \Proof will not print the square.
+
+% Each properly nested Proof/endProof pair gets a single
+% \qedsymbol at the end, on the far right hand side.
+% Unfortunately, this may still be in the wrong place
+% if the proof ends with a display or itemisation.
+% To solve this, \qed may be put *inside* the last substantive
+% environment; the \qedsymbol will be put at that point
+% (the visual end) and suppressed at the logical end of proof.
+
+% Examples:
+% \begin{Proof} \begin{Proof}
+% ... ...
+% \begin{eqnarray} \begin{itemize}
+% ... &=& ... \\ \item ...
+% .. &=& ... &\qed \item ... \qed
+% \end{eqnarray} \end{itemize}
+% \end{Proof} \end{Proof}
+% also works with $$...$$ and \[...\] displays, including fleqn.sty.
+
+% Unfortunately some environments, such as picture, do not allow this at all.
+% See the section "centering environments" below for the mechanism for
+% passing \qed to such an environment for special processing.
+
+% In fact \qed will only work in those environments which provide access to
+% the right hand side of the page. In other words, wherever you think
+% "\hfill\square" ought to work then \qed will; of course it is just because
+% that naive method doesn't work that this macro file is needed at all.
+% The macro was designed to solve the problem in the case of "unrestricted
+% horizontal mode" (ie at the end of a paragraph); it also works in $$
+% displays by pretending to be an equation number. In most other cases it
+% basically does "\hfill\square" or "\hfill$\square$" and hopes for the best.
+
+% If you have to put \qed outside the environment, it may be appropriate to
+% put \vskip-\baselineskip before it, unless of course this would over-print.
+% There is, however, still a danger that TeX will break the page here.
+% This seems to be unavoidable if the environment ends with a \penalty.
+
+% The eqnarray example above does not in fact work: if you try it you'll
+% get "! Paragraph ended before \llap was complete" with LaTeX in a mess.
+% This is a very common place where you might want to put the end of proof
+% mark, and I also consider that the fourth column should be available for
+% "reasons" for equational steps. The following substitute for \eqnarray
+% allows this, whilst being compatible with automatic numbering. I have
+% proposed it to Rainer Sch\"opf for inclusion in LaTeX. If you want to
+% use it, please copy it to another file rather than uncommenting it here.
+% Don't forget to use \makeatletter or put it in a documentstyle (.sty) file.
+%
+% \def\eqnarray{\stepcounter{equation}\let\@currentlabel\theequation
+% \global\@eqnswtrue\m@th\global\@eqcnt\z@\tabskip\@centering\let\\\@eqncr
+% $$\halign to\displaywidth\bgroup\@eqnsel\hskip\@centering$\displaystyle
+% \tabskip\z@{##}$&\global\@eqcnt\@ne\hskip 2\arraycolsep \hfil${##}$\hfil
+% &\global\@eqcnt\tw@\hskip2\arraycolsep$\displaystyle\tabskip\z@{##}$\hfil
+% \tabskip\@centering&%
+% \global\@eqcnt\thr@@\hbox to\z@\bgroup\hss##%*** instead of "\llap{##}"
+% \tabskip\z@\cr}%
+% \def\@@eqncr{\let\@tempa\relax
+% \ifcase\@eqcnt \def\@tempa{& & &}\or \def\@tempa{& &}%
+% \or\def\@tempa{&}\else\@eqnswfalse%*** instead of "\else\def\@tempa{&}"
+% \fi\@tempa\if@eqnsw\@eqnnum\stepcounter{equation}\fi
+% \egroup%*** added, to match \bgroup in fourth cell of preamble
+% \global\@eqnswtrue\global\@eqcnt\z@\cr}
+
+% Why can't we do all of this with \endProof? Because by that stage
+% the damage has been done: the environments, paragraphs or
+% displays have already been closed and their \hbox'es added
+% to the current vertical list, and cannot be removed for
+% alteration if this is the current page.
+
+% Even if you don't need to put \qed inside an inner environment
+% to avoid a blank line, it's still a good idea to do so, because
+% otherwise it's possible that intervening end-of-environment
+% material may allow TeX to put the mark on the next page.
+
+% This file may be called QED.sty, QED.tex, qed.sty or qed.tex.
+% It may be loaded using \input, \usepackage or as a \documentstyle option,
+% as it is careful to handle the \catcode of @ appropriately.
+
+% If you don't use theorem.sty, this file instead provides options to use
+% commands to begin theorems, instead of enclosing them in environments,
+% and to suppress numbering and italicisation. A rudimentary version of
+% \newtheorem for plain TeX is also implemented (always using commands
+% rather than environments).
+
+% At the end of the file some useful \newtheorem
+% commands are listed but not executed.
+
+% NB \Theorem\Proof\endProof\qed will print the second square, whereas
+% \begin{Theorem}\end{Theorem}\begin{Proof}\end{Proof}\qed will not.
+
+%=========================================================================
+% Make @ letter, saving its old code to restore at the end of this file.
+% Look for this towards the end of the file if you think something's missing!
+% "plain.tex" defines \lq as a synonym for back quote (character constant);
+% I use it to avoid corruption when sending TeX files by email via BITNET.
+\edef\qedrestoreat{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}%%
+\catcode\lq\@=11
+
+% in LaTeX, \protect the user commands;
+% in plain TeX, ensure that it is defined.
+\ifx\protect\undefined\let\protect\relax\fi
+
+%=========================================================================
+
+% OPTIONS
+
+% These are the user commands.
+
+\def\qed{\protect\@qed{$\qedsymbol$}}% suppressible printing of \qedsymbol
+% \pushright takes an argument, which it always prints
+% it is (re)defined by \WillHandleQED and \UnHandleQED below (12.4.94)
+
+% theoremata in Euclid needed proof: "which was to be shown"
+\def\QED{\protect\@qed{{\rm Q.E.D.}}}% "quod erat demonstrandum"
+
+% but problemata needed construction: "which was to be found"
+\def\QEI{\protect\@qed{{\rm Q.E.I.}}}% "quod erat inveniendum"
+
+% alternatively: "which was to be done/made"
+\def\QEF{\protect\@qed{{\rm Q.E.F.}}}% "quod erat faciendum"
+
+% a LaTeX environment
+\def\Proof{\protect\@Proof}\def\endProof{\protect\@endProof}%
+\let\proof\Proof\let\endproof\endProof
+
+
+% These are the user-settable parameters.
+
+% The actual (maths) symbol used by \qed
+\def\qedsymbol{\square}% PLEASE NOTE: this is in the AMS symbols font.
+%\def\qedsymbol{\blacksquare}% use one of these instead
+%\def\qedsymbol{\hbox{\rm Q.E.D.}}% if you prefer
+%\def\qedsymbol{\dashv}% this is what the Journal of Symbolc Logic likes.
+
+% This is the text used by \Proof.
+% A new paragraph is begun without indentation.
+% Change it to {\kern\parindent\sc D\'emonstration: } if you like.
+\def\TheWordProof{\bf Proof\enskip}
+
+% This is the font command used for the text of proofs
+\def\ProofFont{}
+
+% The command \AutoQEDtrue causes a \qed in \end{Theorem}, so you do
+% \begin{Theorem} ... \begin{Proof} ... \end{Proof} \end{Theorem}
+% but if you omit the proof, the statement gets a little square at the end.
+\newif\ifAutoQED\AutoQEDfalse
+
+% The remaining options are redundant with theorem.sty
+% so are not defined if this has been loaded.
+\newif\ifNumberResults
+\ifx\theorem@style\undefined
+ %
+ % How to print the name (#1), number (#2) and attribution (#3) of a theorem.
+ \NumberResultstrue
+ % If the number (#2) is absent, "\unskip" removes the
+ % unwanted space "\ " from before it (16 Feb 1993).
+ \def\TheoremHeader#1#2#3{\bf #1\ifNumberResults\ #2\unskip\fi#3}
+ %
+ % This is the font command used for the text of theorem enunciations
+ % change to {\rm} or {\small} if you like.
+ \def\TheoremFont{\it}
+ %
+ % The command \NumberResultsfalse will suppress theorem numbering.
+ %
+ % The command \TheoremsAsCommands will allow you to write
+ % \Theorem instead of \begin{Theorem} ... \end{Theorem}.
+ % In this case italicisation is suppressed by default.
+ % To do this with theorem.sty would involve rewriting the substyles.
+ %
+ % WARNING: if you subsequently redefine \TheoremFont, and use the command
+ % instead of the environment, the font will remain in force afterwards!
+\fi
+
+% The document style option "theorems-as-commands" will allow you to
+% write \Theorem instead of \begin{Theorem} ... \end{Theorem}.
+% Moved here from further down. 10 Jan 1994
+\def\TheoremsAsCommands{%
+ \def\TheoremFont{}% suppress italicised theorems.
+ \def\begin@theorem##1{%
+ \par\removelastskip\smallskip
+ \save@set@qed % enable \qed
+ \noindent{##1}% the name
+ %\TheoremFont % italicise at your own risk!
+ }%
+ \def\@endtheorem{\ifAutoQED\qed\fi\restore@qed}%
+}%
+
+\expandafter\let\csname ds@theorems-as-commands\endcsname\TheoremsAsCommands
+
+%=========================================================================
+% If you already have a macro called \qed, \endproof or \pushright
+% which is laid out in a similar way to the following two definitions
+% (but with \hbox@pushright incorporated) then it is almost certainly
+% my code, which has been copied anonymously via numerous people since
+% my Cambridge PhD thesis in August 1986. Belated acknowledgements to
+% Chris Thompson of the Cambridge University Computing Service for his
+% help with my early attempts at TeX, in particular this problem.
+
+% The complexity of the macro necessary to get a little box on the
+% right-hand-side at the end of a proof is amazing. It really does
+% have to be this long! Otherwise you're liable to get it at the
+% beginning of the next line, or even on the next page.
+
+\def\parag@pushright#1{{% set up
+ \parfillskip=0pt % so \par doesnt push \square to left
+ \widowpenalty=10000 % so we dont break the page before \square
+ \displaywidowpenalty=10000 % ditto
+ \finalhyphendemerits=0 % TeXbook exercise 14.32
+ %
+ % horizontal
+ %\leavevmode % not needed since we now only use it in hmode
+ \hbox@pushright % this used to be incorporated
+ #1% % the end-of-proof mark (or whatever)
+ %
+ % vertical
+ \par}}% % build paragraph with the above parameters
+
+\def\hbox@pushright{% horizontal
+ \unskip % remove previous space or glue
+ \nobreak % don't break lines
+ \hfil % ragged right if we spill over
+ \penalty50 % discouragement to do so
+ \hskip.2em % ensure some space
+ \null % anchor the following \hfill
+ \hfill % push \square to right
+}%
+
+% Ideally \endProof should do all this. We should be able to add the symbol
+% to the last line after the paragraph, display or whatever other structure
+% has been completed and we've returned to vertical mode. This isn't possible
+% on the current page (outer vmode) because \lastbox doesn't work there.
+
+% But \ifinner is true inside a \vbox, \vadjust or \insert (LaTeX \parbox,
+% minipage, figure or table), and in these circumstances we can use \lastbox.
+% We would have to strip & restore glue & penalties (\insert, \mark and \write
+% are obstacles to this) to get access to the last line (box), which may
+% still not have the correct baseline. We could check its natural width
+% against the page width, but if we re-set it, centering and (right)
+% justification might be disturbed. Is this worth the trouble?
+\def\vbox@pushright#1{\expandafter\message % (2 Jan 1994)
+ {QED.sty could be improved in this case (line \the\inputlineno): please ask}%
+ \page@pushright{#1}}%
+
+% Using this method the Proof environment could be implemented by collecting
+% the entire proof in its own \vbox, modifying that and \unvbox'ing it to the
+% current page. This approach may lead to the following problems:
+% (i) footnotes, floats, marginpars, labels and index items may be lost;
+% (ii) overflow of TeX's main memory, especially if \end{Proof} is missing;
+% (iii) I don't know how page-breaking would be handled.
+
+%========================================================================
+
+% Switch to enable/suppress \qedsymbol; since suppression may be done
+% within a nested scope it must be global, so we do our own save/restore
+% in a symbol which is local to the Proof environment.
+% On first use, we check to see whether an obsolete version of Paul.sty
+% is around, and complain loudly if it is, because they interfere seriously.
+
+\newif\if@qed\@qedfalse
+\def\save@set@qed{\check@pt@sty@v\let\saved@ifqed\if@qed\global\@qedtrue}%
+\def\restore@qed{\global\let\if@qed\saved@ifqed}
+
+% prefer proofs with statements if possible - hence \penalty700
+% the only essential part of this is \save@set@qed
+\def\@Proof{%
+ \par\removelastskip\smallskip\penalty700
+ \save@set@qed
+ \noindent\ProofFont{\TheWordProof\enskip}%
+}%
+
+\def\@endProof{%
+ \qed\restore@qed
+ \penalty-700 \smallskip
+}
+
+\def\@qed#1{\check@pt@fm@thm
+\if@qed % have we already done \qed?
+ \global\@qedfalse\pushright{#1}% - no - do it now, but not again
+\else\ifhmode\ifinner\else\par\fi\fi% - yes - just end paragraph, if any
+\fi}
+
+% \pushright{text} always prints its argument, on the far right, in text mode
+\def\@pushright#1{%
+ \ifvmode
+ \ifinner\vbox@pushright{#1}% vertical mode (see comments above)
+ \else \page@pushright{#1}%
+ \fi
+ \else\ifmmode\maths@pushright{\hbox{#1}}% maths (force a text argument)
+ \else\ifinner\hbox@pushright{#1}% inside an \hbox
+ \else\parag@pushright{#1}% in a paragraph
+ \fi \fi \fi
+}% (22 Feb 1993) removed extra {} which would destroy our \] below
+
+% In the \hbox and maths cases we are really at the mercy of the environment.
+% Assuming that we have $\qed$ simply embedded in a paragraph, the horizontal
+% processing by \hbox@pushright will at least make sure that the square isn't
+% at the beginning of the line, but we can't stop it being on the next page.
+% However it is more likely that the reason why we're in maths mode is that
+% we're inside an eqnarray or similar, in which case \hfill will do its best
+% to put the square on the right of the available space. (See \vadjust below.)
+\def\maths@pushright#1{%
+ \ifinner
+ \hbox@pushright{#1}%
+ \else
+ \eqno#1% use TeX's right equation number feature (\eqno) within $$.
+ \def\]{$$\ignorespaces}% suppress LaTeX's error checking (HACK!)
+ \fi
+}% (22 Feb 1993) removed extra {} which would destroy our \] above
+
+% outer vertical mode (the current page)
+% There's very little we can do in these circumstances!
+% Penalties still allow the page to be broken.
+% If the user has put negative glue in, leave it alone. (15 Feb 1994)
+\def\page@pushright#1{% 18 Jan 1994
+ %\unpenalty % ineffective
+ \skip@\lastskip
+ \ifdim\skip@>\z@
+ \unskip % remove \parskip, but only (15 Feb 1994) if it's positive
+ \else\skip@\z@\relax
+ \fi
+ %\unpenalty % TeX won't let me do this
+ \dimen@\baselineskip
+ \advance\dimen@-\prevdepth % save \prevdepth to make a strut
+ \nobreak % don't break the page here
+ \nointerlineskip
+ \hbox to\hsize{%
+ \setbox\z@\null
+ \ifdim\dimen@>\z@\ht\z@\dimen@\fi % simulate \baselineskip
+ \box\z@
+ \hfill
+ #1}%
+ \vskip\skip@ % replace old \parskip
+}%
+
+% An idea that didn't work: see TeXbook p188. (16 Feb 1993)
+% Use \predisplaysize to find out the width of the previous box,
+% in the case where it has already been completed.
+% But this can only be used inside displays ($$), and a display in
+% vertical mode begins a paragraph first, so we end up with
+% \predisplaysize=\parindent+2em whatever happened in the previous
+% paragraph.
+
+% Another idea: it may be worth trying \vadjust, if only to insert \nobreak.
+% The problem with this is that if we are too deeply nested in horizontal
+% or maths lists, the adjustment may not be able to find its way out to the
+% enclosing vertical list. In the case of array-like environments, it will
+% appear (assuming it manages to get out) after the current row of the array.
+
+%===========================================================================
+% We have to add to the theorem environments the commands to enable \qed.
+% This is done by re-defining \@thm#1#2.
+% Note that Mittelbach's theorem.sty re-defines \@thm and \@endtheorem, so
+% that must be loaded before us, otherwise our changes will get over-written
+% and \qed will never be enabled.
+% Paul.sty didn't use this method of gaining control inside a theorem,
+% whereas it did define \qed and \pushright, so here is the one place
+% where we can check for it.
+
+\ifx\nonqed@thm\undefined % otherwise double loading causes a loop 22 Feb 1993
+ \let\nonqed@thm\@thm % save original
+ \let\nonqed@endthm\@endtheorem
+\fi
+
+\def\@thm{\save@set@qed\nonqed@thm}%
+\def\@endtheorem{\ifAutoQED\qed\fi\restore@qed\nonqed@endthm}%
+
+%===========================================================================
+% "CENTERING" ENVIRONMENTS -
+% those which don't give their contents access to the right hand side
+% of the page, such as center, picture, ... (12 April 1994)
+
+% Each individual environment (both the standard ones and those defined
+% by the user) needs to co-operate in order to make \qed and \pushright work.
+% It is not the business of this package to rewrite LaTeX in this way,
+% but the following mechanism may be inserted in to other environments.
+% - put \WillHandleQED in the \begin part of the environment definition;
+% then if a \qed occurs in the body of the environment it is stored
+% in \QEDbox until...
+% - \HandleQED anywhere in the \end part of the environment definition
+% (even inside dollars, braces or another environment) prints it.
+%
+% For example:
+% \newenvironment{qedpicture}%
+% {\begin{picture}\WillHandleQED}%
+% {\put(0,0){\HandleQED}\end{picture}}
+%
+% To make this compatible with *not* loading QED.sty,
+% add the following to macro files which use \WillHandleQED and \HandleQED:
+% \ifx\WillHandleQED\undefined
+% \let\WillHandleQED\relax
+% \let\HandleQED\relax
+% \let\UnHandleQED\relax % if you use it
+% \let\QEDbox\voidb@x % must have \makeatletter here!
+% \fi
+%
+% \UnHandleQED restores normal processing; this may be useful for
+% the minipage environment, which has its own notion of "right hand side"
+% of the page.
+%
+% The width of the saved \qed is available for testing as \wd\QEDbox
+
+\newbox\qed@box % the box in which to save \qed for special handling
+
+\def\WillHandleQED{\relax
+\ifx\HandleQED\nohandle@qed
+ % no enclosing environment has declared \WillHandleQED
+ \def\pushright{\global\setbox\qed@box\hbox}% \qed will be saved
+ \let\QEDbox\qed@box % point at the right box
+ \def\HandleQED{\unhbox\QEDbox}% print it
+ \aftergroup\check@handle@qed % check that this really gets done
+\else
+ % an enclosing environment already wants to catch \qed
+ % \HandleQED doesn't print anything - let the saved \qed pass through
+ \let\QEDbox\voidb@x % by pointing at an empty box
+\fi}
+
+\def\nohandle@qed{%
+\errhelp{One of them is missing: see QED.sty.}%
+\errmessage{This environment uses \string\WillHandleQED\space and
+\string\HandleQED\space incorrectly}}
+
+\def\check@handle@qed{\relax
+\ifvoid\qed@box\else\expandafter\nohandle@qed\fi}
+
+\def\UnHandleQED{%
+\let\HandleQED\nohandle@qed
+\let\QEDbox\voidb@x
+\def\pushright{\protect\@pushright}}%
+
+\UnHandleQED
+
+%===========================================================================
+% Check for obsolete versions and clashes of this and other macro files.
+% Why do I do this? Because of those people who complain to me that
+% something doesn't work but refuse to read the manual, and those
+% who refuse to update their software, and then publish papers with
+% commutative diagrams full of the bugs which I fixed several years ago.
+
+\def\obsolete@pt@version#1{\errhelp={%
+% *****************************************************************
+% * The master version is available by *
+ Anonymous FTP ftp.dcs.qmw.ac.uk /pub/tex/contrib/pt/tex/#1}%*
+% *****************************************************************
+\errmessage{You have an obsolete version of #1 - please get a new one}}%
+
+% First check QED.sty
+%\ifnum\year>1996 \obsolete@pt@version{QED.sty}\fi
+
+% If theorem.sty hasn't been loaded, arrange to check it again in \@qed.
+% And check (then) whether you've actually defined \square.
+% changed 2 June 1993: don't define it now, as that would confuse amssymb.sty
+\ifx\theorem@style\undefined
+ \def\check@pt@fm@thm{\relax
+ \ifx\square\undefined
+ \gdef\square{\bigcirc
+ \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
+ \errmessage{\string\square\space is an AMS symbol}%
+ \global\let\square\bigcirc}%
+ \fi
+ \ifx\theorem@style\undefined
+ \global\let\check@pt@fm@thm\relax
+ \else\errhelp={The macros \@thm and \@endtheorem need to be re-defined.}%
+ \errmessage{QED.sty must be loaded AFTER theorem.sty but before
+ using \string\newtheorem}%
+ \fi
+ \global\let\check@pt@fm@thm\relax
+ }%
+\else
+ \def\check@pt@fm@thm{%
+ \ifx\square\undefined
+ \def\square{\bigcirc
+ \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
+ \errmessage{\string\square\space is an AMS symbol}%
+ \global\let\square\bigcirc}%
+ \fi
+ \global\let\check@pt@fm@thm\relax
+ }%
+\fi
+
+% Check for Paul.sty, which SERIOUSLY conflicts with this file.
+% and also for version 2 or version 3 of commutative diagrams.
+\def\check@pt@sty@v{%
+ \relax
+ \ifx\@@begintheorem\undefined
+ \else\message{*** QED.sty and the old Paul.sty seriously conflict! ***}%
+ \obsolete@pt@version{Paul.sty}%
+ \fi
+ \ifx\execHorizontalMap\undefined
+ \gdef\obsolete@pt@version##1{}% it's no longer needed
+ \else\global\let\di@gr@m\diagram
+ \gdef\diagram{\obsolete@pt@version{diagrams.tex}\di@gr@m}%
+ \fi
+ \global\let\check@pt@sty@v\relax
+}%
+
+%===========================================================================
+
+% Define some standard ``theorem'' types.
+
+\def\DefineStandardTheorems{%
+%
+% First set up uniform numbering in LaTeX;
+% don't use this in plain TeX because this usage of \newcommand is not
+% supported and we have already done by hand what it would do in LaTeX,
+% viz to define the macro \theResult and the count \c@Result.
+\relax\ifx\@@thm\undefined
+ \newtheorem{Result}{Result}[subsection]%
+ \@addtoreset{Result}{section}%
+ \ifx\chapter\undefined\else\@addtoreset{Result}{chapter}\fi
+\fi
+%
+\let\theUnnumbered\relax\countdef\c@Unnumbered255 \def\p@Unnumbered{}%
+\let\DefineStandardTheorems\relax
+%
+\newtheorem{Answer}[Result]{Answer}%
+\newtheorem{Answers}[Result]{Answers}%
+\newtheorem{Conjecture}[Result]{Conjecture}%
+\newtheorem{Construction}[Result]{Construction}%
+\newtheorem{Convention}[Unnumbered]{Convention}%
+\newtheorem{Corollary}[Result]{Corollary}%
+\newtheorem{Counterexample}[Result]{Counterexample}%
+\newtheorem{Definition}[Result]{Definition}%
+\newtheorem{Example}[Result]{Example}%
+\newtheorem{Examples}[Result]{Examples}%
+\newtheorem{Exercise}[Result]{Exercise}%
+\newtheorem{Exercises}[Result]{Exercises}%
+\newtheorem{Fact}[Result]{Fact}%
+\newtheorem{Facts}[Result]{Facts}%
+\newtheorem{Lemma}[Result]{Lemma}%
+\newtheorem{NB}[Unnumbered]{NB}%
+\newtheorem{Notation}[Result]{Notation}%
+\newtheorem{Note}[Unnumbered]{Note}%
+\newtheorem{Observation}[Result]{Observation}%
+\newtheorem{Observations}[Result]{Observations}%
+\newtheorem{Problem}[Result]{Problem}%
+\newtheorem{Proposition}[Result]{Proposition}%
+\newtheorem{PS}[Unnumbered]{PS}%
+\newtheorem{Remark}[Result]{Remark}%
+\newtheorem{Question}[Result]{Question}%
+\newtheorem{Questions}[Result]{Questions}%
+\newtheorem{Theorem}[Result]{Theorem}%
+\newtheorem{Thesis}[Result]{Thesis}%
+\newtheorem{Warning}[Result]{Warning}%
+}
+
+%===========================================================================
+% Interaction with LaTeX2e (2 Jan 1994)
+
+\ifx\newtheorem\undefined\else\ifx\ProvidesPackage\undefined
+ \message{^^J^^J}%
+ \message{****************************************************************}%
+ \message{! ***** You are using an obsolete implementation of LaTeX ******}%
+ \message{* A new version - called LaTeX2e - has been available from TeX *}%
+ \message{* FTP archives such as ftp.tex.ac.uk, ftp.uni-stuttgart.de and *}%
+ \message{* pip.shsu.edu since December 1993. It incorporates NFSS2 (the *}%
+ \message{* Mittelbach-Schoepf New Font Selection Scheme) but is reverse *}%
+ \message{* compatible with LaTeX versions 2.09 and is now the standard. *}%
+ \message{****************************************************************}%
+ \message{^^J^^J}%
+\else
+ \ProvidesPackage{QED}[1996/06/24 right-justified end-of-proof mark]%
+ %\ProvidesFile{QED.sty}% I don't understand what this is for
+ \DeclareOption{roman-theorems}{\def\TheoremFont{\rm}}%
+ \DeclareOption{italic-theorems}{\def\TheoremFont{\it}}%
+ \DeclareOption{theorems-as-commands}{\TheoremsAsCommands}%
+ \DeclareOption{auto-QED}{\AutoQEDtrue}%
+ \DeclareOption{explicit-QED}{\AutoQEDfalse}%
+ \DeclareOption{number-theorems}{\NumberResultstrue}%
+ \DeclareOption{dont-number-theorems}{\NumberResultsfalse}%
+ \DeclareOption{black-square}{\def\qedsymbol{\blacksquare}}%
+ \DeclareOption{open-square}{\def\qedsymbol{\square}}%
+ \DeclareOption{define-standard-theorems}{\DefineStandardTheorems}%
+ \ProcessOptions
+\fi\fi
+
+%===========================================================================
+% If Mittelbach's theorem.sty is loaded, skip the rest of the file.
+\ifx\theorem@style\undefined\else\qedrestoreat\expandafter\endinput\fi
+%===========================================================================
+
+% Allow the user to suppress italicisation and numbering.
+
+% The following two macros are called by LaTeX to begin a theorem
+% respectively with and without an optional (``attribution'') argument.
+% It is clear from latex.tex that they are intended to be customised.
+% The code common to the two has been taken out as \begin@theorem and
+% \TheoremHeader. Of these, the former is re-defined by \TheoremsAsCommands.
+
+\def\@opargbegintheorem#1#2#3{\begin@theorem{\TheoremHeader{#1}{#2}{ (#3)} }}
+
+\def\@begintheorem#1#2{\begin@theorem{\TheoremHeader{#1}{#2}{} }}
+
+\def\begin@theorem#1{%
+ \trivlist\item[\hskip\labelsep {#1}]% % LaTeX likes this method.
+ \TheoremFont % Italicise the enunciation
+ \ifx\ProofFont\empty\def\ProofFont{\rm}\fi % but not any nested proof.
+ }%
+
+
+%%% Here's what LaTeX (92/1/14) does:
+%%%% RmS 91/08/14 Moved \it after \item to make it work with NFSS
+%%\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]\it}
+%%\def\@opargbegintheorem#1#2#3{\trivlist
+%% \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]\it}
+%%\def\@endtheorem{\endtrivlist}
+
+
+
+%===========================================================================
+% If we're running under LaTeX, skip the rest of the file.
+\ifx\newtheorem\undefined\else\qedrestoreat\expandafter\endinput\fi
+%===========================================================================
+
+% This implements a rudimentary version of \newtheorem for plain TeX.
+% Only the unattributed theorems and the
+% declarations \newtheorem{Theorem}[Result]{Theorem} and
+% \newtheorem{Convention}[Unnumbered]{Convention} are supported.
+% The numbering is based on the counts \chapternumber, \sectionnumber
+% and \subsectionnumber, which it is up to you to define with \newcount.
+% It's also up to you to reset \c@Result at the beginning of each section.
+
+% Form the number: (chapter).(section).(subsection).(#1)
+% where any of the first three parts which is zero
+% negative or undefined is omitted.
+\def\ther@sult#1{%
+\ifx\chapternumber\undefined\else
+ \ifnum\chapternumber>0 \number\chapternumber.\fi\fi
+\ifx\sectionnumber\undefined\else
+ \ifnum\sectionnumber>0 \number\sectionnumber.\fi\fi
+\ifx\subsectionnumber\undefined\else
+ \ifnum\subsectionnumber>0 \number\subsectionnumber.\fi\fi
+\expandafter\number\csname c@#1\endcsname}%
+
+% plain version of LaTeX's \@thm
+\def\plain@thm#1#2{% #1=counter, #2=text
+ \save@set@qed
+ \expandafter\advance\csname c@#1\endcsname1
+ \@begintheorem{#2}{\csname the#1\endcsname}%
+}%
+
+% Rudimentary \newtheorem
+\def\newtheorem#1[#2]#3{% #1=command, #2=counter, #3=text
+ %
+ % \def\#1{\plain@thm{#2}{#3}}
+ \expandafter\def\csname #1\endcsname{\plain@thm{#2}{#3}}%
+ %
+ % \def\end#1{\@endtheorem}
+ \expandafter\def\csname end#1\endcsname{\@endtheorem}%
+ %
+ % if \c@#2 is not defined
+ % \newcount\c@#2
+ % \def\the#2{\ther@sult{#2}}
+ \expandafter\ifx\csname c@#2\endcsname\relax
+ \expandafter\expandafter\csname newcount\endcsname
+ \csname c@#2\endcsname
+ \expandafter\def\csname the#2\endcsname{\ther@sult{#2}}%
+ \fi
+}%
+
+\TheoremsAsCommands
+
+\qedrestoreat\endinput
+
+%===========================================================================
+% BUGS
+% \item\qed\end{letterlist} puts the square above the item label.
+
+% ! You can't use `\unskip' in vertical mode.
+% from \qed in a paragraph on its own.
diff --git a/macros/generic/proofs/taylor/prooftree-doc.dvi b/macros/generic/proofs/taylor/prooftree-doc.dvi
new file mode 100644
index 0000000000..b126e590c2
--- /dev/null
+++ b/macros/generic/proofs/taylor/prooftree-doc.dvi
Binary files differ
diff --git a/macros/generic/proofs/taylor/prooftree-doc.pdf b/macros/generic/proofs/taylor/prooftree-doc.pdf
new file mode 100644
index 0000000000..ef5cc8c0bb
--- /dev/null
+++ b/macros/generic/proofs/taylor/prooftree-doc.pdf
Binary files differ
diff --git a/macros/generic/proofs/taylor/prooftree-doc.tex b/macros/generic/proofs/taylor/prooftree-doc.tex
new file mode 100644
index 0000000000..a4ed2959b4
--- /dev/null
+++ b/macros/generic/proofs/taylor/prooftree-doc.tex
@@ -0,0 +1,198 @@
+\documentstyle{article}
+\input prooftree
+\title{Build proof tree for Natural Deduction, Sequent Calculus, etc.}
+\author{Paul Taylor\\
+Department of Computing,\\
+Imperial College,\\
+London SW7 2BZ\\
++44 71 589 5111 {\em ext\/} 5057\\
+{\tt<pt@doc.ic.ac.uk>}}
+\def\X{x}
+\let\imp\Rightarrow
+\def\T{{\rm t\!t}}\def\F{{\rm f\!f}}
+\def\P#1{p#1}%
+\def\Q#1{q#1}%
+\def\E#1#2{\exists#2.\X_{#2}={#1}}
+\def\A#1#2{\exists#1.\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)}
+\def\B#1#2{\forall#1.\left(\left(\E{#1}{#2}\right)\imp\P{#1}\right)}
+\def\C#1#2{\exists#1.\P{#1}\land\left(\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)\right)}
+\overfullrule0pt
+\begin{document}
+\maketitle
+Using my Proof Tree macros, you can produce
+{\small
+$$\begin{prooftree}
+\[ \[ [(\A y n)\land(\B w n)]_\alpha
+ \andelim1
+ \A y n
+ \]
+ \kern-26em
+ \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha
+ \andelim2 \shiftright60pt
+ \B w n
+ \]
+ \allelim
+ (\E y n)\imp\P y
+ \]
+ \[
+ [(\E y n)\land\Q y]_\beta
+ \andelim1
+ \E y n
+ \]
+ \impelim \shiftright50pt
+ \P y
+ \]
+ \kern-25pt
+ [(\E y n)\land\Q y]_\beta
+ \andintro
+ \P y\land((\E y n)\land\Q y)
+ \]
+ \existsintro
+ \C z n
+ \]
+ \existselim\beta
+ \C z n
+\]
+\impintro\alpha
+(\A yn)\land(\B w n)\imp(\C z n)
+\end{prooftree}$$}
+using the \TeX\ or \LaTeX\ code
+\begin{verbatim}
+\input prooftree
+$$
+\begin{prooftree}
+\[ \[ [(\A y n)\land(\B w n)]_\alpha
+ \andelim1
+ \A y n
+ \]
+ \kern-26em
+ \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha
+ \andelim2 \shiftright60pt
+ \B w n
+ \]
+ \allelim
+ (\E y n)\imp\P y
+ \]
+ \[
+ [(\E y n)\land\Q y]_\beta
+ \andelim1
+ \E y n
+ \]
+ \impelim \shiftright50pt
+ \P y
+ \]
+ \kern-25pt
+ [(\E y n)\land\Q y]_\beta
+ \andintro
+ \P y\land((\E y n)\land\Q y)
+ \]
+ \existsintro
+ \C z n
+ \]
+ \existselim\beta
+ \C z n
+\]
+\impintro\alpha
+(\A yn)\land(\B w n)\imp(\C z n)
+\end{prooftree}$$
+\end{verbatim}
+
+
+
+In fact the commands \verb/\allintro/, {\it etc.,} are not primitive;
+the basic form is
+\begin{verbatim}
+\[
+ A\quad
+ B
+\justifies
+ A \land B
+\thickness=0.08em
+\shiftright 2em
+\using
+ {\land}{\cal I}
+\]
+\end{verbatim}
+which gives
+$$\begin{prooftree}
+ A\quad
+ B
+\justifies
+ A \land B
+\thickness=0.08em
+\shiftright 2em
+\using
+ {\land}{\cal I}
+\end{prooftree}$$
+The hypotheses may themselves be proof trees (enclosed in
+\verb/\[/\ldots\verb/\]/)
+and the purpose of the macros is to adjust
+the length of the horizontal ``deduction'' line. When the hypotheses
+are proof trees, suitable space is put between them, but of course
+this must be supplied by hand for simple formulae. The \verb/\thickness/
+and \verb/\shiftright/ commands are, of course, optional; they apply to
+the horizontal line and to the positioning of the conclusion relative to
+it. For a double line, use \verb/\Justifies/ instead of \verb/\justifies/.
+
+Notice the overloading of the \verb/\[/\ldots\verb/\]/; the outermost proof
+tree must be enclosed with \verb/\begin{prooftree}/ and \verb/\end{prooftree}/
+or \verb/\prooftree/ and \verb/\endprooftree/.
+
+To get a vertical string of dots instead of the proof rule, do
+\begin{verbatim}
+\[
+ [A]
+\using
+ \pi
+\proofdotseparation=1.2ex
+\proofdotnumber=4
+\leadsto
+ B
+\]
+\end{verbatim}
+to get
+\prooftree
+ [A]
+\using
+ \pi
+\proofdotseparation=1.2ex
+\proofdotnumber=4
+\leadsto
+ B
+\endprooftree
+
+All of of the keywords except \verb/\prooftree/ and \verb/\endprooftree/
+are optional and may appear in any order. They may also be combined in
+\verb/\newcommand/s, for example
+\begin{verbatim}
+\newcommand\Cut{\using\sf cut\thickness.08em\justifies}
+\end{verbatim}
+with the abbreviation
+\begin{verbatim}
+\[ A \vdash B \qquad
+ B \vdash C
+ \Cut
+ A \vdash C
+\]
+\end{verbatim}
+
+\verb/\thickness/ specifies the breadth of the rule in any units, although
+font-relative units such as ex or em are preferable.
+It may optionally be followed by =.
+\verb/\proofrulebreadth=.08em/ or \verb/\setlength\proofrulebreadth{.08em}/
+may also be used either in place of \verb/\thickness/ or globally; the
+default is 0.04em. \verb/\proofdotseparation/ and \verb/\proofdotnumber/
+control the size of the string of dots.
+
+If proof trees and formulae are mixed, some explicit spacing is needed,
+but don't put anything to the left of the left-most (or the right of
+the right-most) hypothesis, or put it in braces, because this will cause
+the indentation to be lost.
+
+By default the conclusion is centered wrt the left-most and right-most
+immediate hypotheses (not their proofs); \verb/\shiftright/ or
+\verb/\shiftleft/ moves it relative to this position.
+(Not sure about this specification or how
+it should affect spreading of proof tree.)
+
+\end{document} \ No newline at end of file
diff --git a/macros/generic/proofs/taylor/prooftree.sty b/macros/generic/proofs/taylor/prooftree.sty
new file mode 120000
index 0000000000..7d6ff36ab3
--- /dev/null
+++ b/macros/generic/proofs/taylor/prooftree.sty
@@ -0,0 +1 @@
+prooftree.tex \ No newline at end of file
diff --git a/macros/generic/proofs/taylor/prooftree.tex b/macros/generic/proofs/taylor/prooftree.tex
new file mode 100644
index 0000000000..abb7d44864
--- /dev/null
+++ b/macros/generic/proofs/taylor/prooftree.tex
@@ -0,0 +1,347 @@
+\message{<Paul Taylor's Proof Trees, 2 August 1996>}
+%% Build proof tree for Natural Deduction, Sequent Calculus, etc.
+%% WITH SHORTENING OF PROOF RULES!
+%% Paul Taylor, begun 10 Oct 1989
+%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! ***
+%%
+%% 2 Aug 1996: fixed \mscount and \proofdotnumber
+%%
+%% \prooftree
+%% hyp1 produces:
+%% hyp2
+%% hyp3 hyp1 hyp2 hyp3
+%% \justifies -------------------- rulename
+%% concl concl
+%% \thickness=0.08em
+%% \shiftright 2em
+%% \using
+%% rulename
+%% \endprooftree
+%%
+%% where the hypotheses may be similar structures or just formulae.
+%%
+%% To get a vertical string of dots instead of the proof rule, do
+%%
+%% \prooftree which produces:
+%% [hyp]
+%% \using [hyp]
+%% name .
+%% \proofdotseparation=1.2ex .name
+%% \proofdotnumber=4 .
+%% \leadsto .
+%% concl concl
+%% \endprooftree
+%%
+%% Within a prooftree, \[ and \] may be used instead of \prooftree and
+%% \endprooftree; this is not permitted at the outer level because it
+%% conflicts with LaTeX. Also,
+%% \Justifies
+%% produces a double line. In LaTeX you can use \begin{prooftree} and
+%% \end{prootree} at the outer level (however this will not work for the inner
+%% levels, but in any case why would you want to be so verbose?).
+%%
+%% All of of the keywords except \prooftree and \endprooftree are optional
+%% and may appear in any order. They may also be combined in \newcommand's
+%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation
+%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and
+%% some standard abbreviations will be found at the end of this file.
+%%
+%% \thickness specifies the breadth of the rule in any units, although
+%% font-relative units such as "ex" or "em" are preferable.
+%% It may optionally be followed by "=".
+%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be
+%% used either in place of \thickness or globally; the default is 0.04em.
+%% \proofdotseparation and \proofdotnumber control the size of the
+%% string of dots
+%%
+%% If proof trees and formulae are mixed, some explicit spacing is needed,
+%% but don't put anything to the left of the left-most (or the right of
+%% the right-most) hypothesis, or put it in braces, because this will cause
+%% the indentation to be lost.
+%%
+%% By default the conclusion is centered wrt the left-most and right-most
+%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves
+%% it relative to this position. (Not sure about this specification or how
+%% it should affect spreading of proof tree.)
+%
+% global assignments to dimensions seem to have the effect of stretching
+% diagrams horizontally.
+%
+%%==========================================================================
+
+\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%%
+\def\andintro{\using{\land}\introrule\justifies}%%
+\def\impelim{\using{\Rightarrow}\elimrule\justifies}%%
+\def\allintro{\using{\forall}\introrule\justifies}%%
+\def\allelim{\using{\forall}\elimrule\justifies}%%
+\def\falseelim{\using{\bot}\elimrule\justifies}%%
+\def\existsintro{\using{\exists}\introrule\justifies}%%
+
+%% #1 is meant to be 1 or 2 for the first or second formula
+\def\andelim#1{\using{\land}#1\elimrule\justifies}%%
+\def\orintro#1{\using{\lor}#1\introrule\justifies}%%
+
+%% #1 is meant to be a label corresponding to the discharged hypothesis/es
+\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%%
+\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%%
+\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies}
+
+%%==========================================================================
+
+\newdimen\proofrulebreadth \proofrulebreadth=.05em
+\newdimen\proofdotseparation \proofdotseparation=1.25ex
+\newdimen\proofrulebaseline \proofrulebaseline=2ex
+\newcount\proofdotnumber \proofdotnumber=3
+\let\then\relax
+\def\hfi{\hskip0pt plus.0001fil}
+\mathchardef\squigto="3A3B
+%
+% flag where we are
+\newif\ifinsideprooftree\insideprooftreefalse
+\newif\ifonleftofproofrule\onleftofproofrulefalse
+\newif\ifproofdots\proofdotsfalse
+\newif\ifdoubleproof\doubleprooffalse
+\let\wereinproofbit\relax
+%
+% dimensions and boxes of bits
+\newdimen\shortenproofleft
+\newdimen\shortenproofright
+\newdimen\proofbelowshift
+\newbox\proofabove
+\newbox\proofbelow
+\newbox\proofrulename
+%
+% miscellaneous commands for setting values
+\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 }
+\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }%
+\afterassignment\setshiftproofbelow\dimen0 }
+\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 }
+\def\setproofrulebreadth{\proofrulebreadth}
+
+%=============================================================================
+\def\prooftree{% NESTED ZERO (\ifonleftofproofrule)
+%
+% first find out whether we're at the left-hand end of a proof rule
+\ifnum \lastpenalty=1
+\then \unpenalty
+\else \onleftofproofrulefalse
+\fi
+%
+% some space on left (except if we're on left, and no infinity for outermost)
+\ifonleftofproofrule
+\else \ifinsideprooftree
+ \then \hskip.5em plus1fil
+ \fi
+\fi
+%
+% begin our proof tree environment
+\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove,
+% \shortenproofleft, \shortenproofright, \proofrulebreadth)
+\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}%
+\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl
+\let\using\proofusing\let\[\prooftree
+\ifinsideprooftree\let\]\endprooftree\fi
+\proofdotsfalse\doubleprooffalse
+\let\thickness\setproofrulebreadth
+\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow
+\let\shiftleft\shiftproofbelowneg
+\let\ifwasinsideprooftree\ifinsideprooftree
+\insideprooftreetrue
+%
+% now begin to set the top of the rule (definitions local to it)
+\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO
+\let\wereinproofbit\prooftree
+%
+% these local variables will be copied out:
+\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt
+%
+% flags to enable inner proof tree to detect if on left:
+\onleftofproofruletrue\penalty1
+}
+
+%=============================================================================
+% end whatever box and copy crucial values out of it
+\def\eproofbit{% NESTED TWO
+%
+% various hacks applicable to hypothesis list
+\ifx \wereinproofbit\prooftree
+\then \ifcase \lastpenalty
+ \then \shortenproofright=0pt % 0: some other object, no indentation
+ \or \unpenalty\hfil % 1: empty hypotheses, just glue
+ \or \unpenalty\unskip % 2: just had a tree, remove glue
+ \else \shortenproofright=0pt % eh?
+ \fi
+\fi
+%
+% pass out crucial values from scope
+\global\dimen0=\shortenproofleft
+\global\dimen1=\shortenproofright
+\global\dimen2=\proofrulebreadth
+\global\dimen3=\proofbelowshift
+\global\dimen4=\proofdotseparation
+\global\count255=\proofdotnumber
+%
+% end the box
+$\egroup % NESTED ONE
+%
+% restore the values
+\shortenproofleft=\dimen0
+\shortenproofright=\dimen1
+\proofrulebreadth=\dimen2
+\proofbelowshift=\dimen3
+\proofdotseparation=\dimen4
+\proofdotnumber=\count255
+}
+
+%=============================================================================
+\def\proofover{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofover
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdbl{% NESTED TWO
+\eproofbit % NESTED ONE
+\doubleprooftrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdbl
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdots{% NESTED TWO
+\eproofbit % NESTED ONE
+\proofdotstrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdots
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofusing{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofrulename=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofusing
+\kern0.3em$
+}
+
+%=============================================================================
+\def\endprooftree{% NESTED TWO
+\eproofbit % NESTED ONE
+% \dimen0 = length of proof rule
+% \dimen1 = indentation of conclusion wrt rule
+% \dimen2 = new \shortenproofleft, ie indentation of conclusion
+% \dimen3 = new \shortenproofright, ie
+% space on right of conclusion to end of tree
+% \dimen4 = space on right of conclusion below rule
+ \dimen5 =0pt% spread of hypotheses
+% \dimen6, \dimen7 = height & depth of rule
+%
+% length of rule needed by proof above
+\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft
+\advance\dimen0-\shortenproofright
+%
+% amount of spare space below
+\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow
+\dimen4=\dimen1
+\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift
+%
+% conclusion sticks out to left of immediate hypotheses
+\ifdim \dimen1<0pt
+\then \advance\shortenproofleft\dimen1
+ \advance\dimen0-\dimen1
+ \dimen1=0pt
+% now it sticks out to left of tree!
+ \ifdim \shortenproofleft<0pt
+ \then \setbox\proofabove=\hbox{%
+ \kern-\shortenproofleft\unhbox\proofabove}%
+ \shortenproofleft=0pt
+ \fi
+\fi
+%
+% and to the right
+\ifdim \dimen4<0pt
+\then \advance\shortenproofright\dimen4
+ \advance\dimen0-\dimen4
+ \dimen4=0pt
+\fi
+%
+% make sure enough space for label
+\ifdim \shortenproofright<\wd\proofrulename
+\then \shortenproofright=\wd\proofrulename
+\fi
+%
+% calculate new indentations
+\dimen2=\shortenproofleft \advance\dimen2 by\dimen1
+\dimen3=\shortenproofright\advance\dimen3 by\dimen4
+%
+% make the rule or dots, with name attached
+\ifproofdots
+\then
+ \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0
+ \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}%
+ \setbox0=\hbox{%
+ \advance\dimen6-.5\wd1
+ \kern\dimen6
+ $\vcenter to\proofdotnumber\proofdotseparation
+ {\leaders\box1\vfill}$%
+ \unhbox\proofrulename}%
+\else \dimen6=\fontdimen22\the\textfont2 % height of maths axis
+ \dimen7=\dimen6
+ \advance\dimen6by.5\proofrulebreadth
+ \advance\dimen7by-.5\proofrulebreadth
+ \setbox0=\hbox{%
+ \kern\shortenproofleft
+ \ifdoubleproof
+ \then \hbox to\dimen0{%
+ $\mathsurround0pt\mathord=\mkern-6mu%
+ \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill
+ \mkern-6mu\mathord=$}%
+ \else \vrule height\dimen6 depth-\dimen7 width\dimen0
+ \fi
+ \unhbox\proofrulename}%
+ \ht0=\dimen6 \dp0=-\dimen7
+\fi
+%
+% set up to centre outermost tree only
+\let\doll\relax
+\ifwasinsideprooftree
+\then \let\VBOX\vbox
+\else \ifmmode\else$\let\doll=$\fi
+ \let\VBOX\vcenter
+\fi
+% this \vbox or \vcenter is the actual output:
+\VBOX {\baselineskip\proofrulebaseline \lineskip.2ex
+ \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi
+ \hbox spread\dimen5 {\hfi\unhbox\proofabove\hfi}%
+ \hbox{\box0}%
+ \hbox {\kern\dimen2 \box\proofbelow}}\doll%
+%
+% pass new indentations out of scope
+\global\dimen2=\dimen2
+\global\dimen3=\dimen3
+\egroup % NESTED ZERO
+\ifonleftofproofrule
+\then \shortenproofleft=\dimen2
+\fi
+\shortenproofright=\dimen3
+%
+% some space on right and flag we've just made a tree
+\onleftofproofrulefalse
+\ifinsideprooftree
+\then \hskip.5em plus 1fil \penalty2
+\fi
+}
+
+%==========================================================================
+% IDEAS
+% 1. Specification of \shiftright and how to spread trees.
+% 2. Spacing command \m which causes 1em+1fil spacing, over-riding
+% exisiting space on sides of trees and not affecting the
+% detection of being on the left or right.
+% 3. Hack using \@currenvir to detect LaTeX environment; have to
+% use \aftergroup to pass \shortenproofleft/right out.
+% 4. (Pie in the sky) detect how much trees can be "tucked in"
+% 5. Discharged hypotheses (diagonal lines).