%
% prftree.sty
% by Marco Benini - 30th November 2014
%
% A package to typeset natural deduction proofs, or sequent proofs, or
% tableau proofs
%
% This package is distributed under the GNU General Public License
%

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{prftree}[2014/11/30 Natural Deduction Proofs]

% Package options
\newif\ifprf@NDOption\prf@NDOptionfalse
\newif\ifprf@SEQOption\prf@SEQOptionfalse
\newif\ifprfIMPOption\prfIMPOptionfalse

\DeclareOption{ND}{\prf@NDOptiontrue}
\DeclareOption{SEQ}{\prf@SEQOptiontrue}
\DeclareOption{IMP}{\prf@IMPOptiontrue}
\ProcessOptions\relax

%--------------------------------------------------------------------
% A proof tree is composed by a generic cell:
%  A1 A2 A3
% ---------- R
%      C
% We call A1, A2, A3. ... assumptions, C the conclusion and R the rule
% name. The line dividing the assumptions from the conclusion is
% called the proof line. A proof tree with no assumptions is an axiom.
% An assumption which is not a proof tree is a pure assumption.
%
% A proof tree is typeset by
% \prftree[<options>]...[<options>]
%         {<assumption1>}...{<assumptionN>}
%         {<conclusion>}
% The possible options are:
%   r             : the first argument after the options is the rule
%                   name, typeset in text mode
%   rule          : synonym for 'r'
%   by rule       : synonym for 'r'
%   by            : synonym for 'r'
%   right         : synonym for 'r'
%   l             : the first argument after the options is the rule
%                   label, typeset in text mode; if there is also a
%                   rule name, the label is the second argument
%   label         : synonym for 'l'
%   left          : synonym for 'l'
%   straight      : the proof line will be a solid line (default) 
%   straight line : synonym for 'l'
%   straightline  : synonym for 'l'
%   dotted        : the proof line will be a dotted line
%   dotted line   : synonym for 'dotted'
%   dottedline    : synonym for 'dotted'
%   dashed        : the proof line will be a dashed line
%   dashed line   : synonym for 'dashed'
%   dashedline    : synonym for 'dashed'
%   f             : the proof line will be fancy
%   fancy         : synonym for 'f'
%   fancy line    : synonym for 'f'
%   fancyline     : synonym for 'f'
%   s             : the proof line will be single, not double (default)
%   single        : synonym for 's'
%   single line   : synonym for 's'
%   singleline    : synonym for 's'
%   d             : the proof line will be double, not single
%   double        : synonym for 'd'
%   double line   : synonym for 'd'
%   doubleline    : synonym for 'd'
%   noline        : suppresses the proof line (prevails over all other
%                   line options)
%   summary       : renders the proof line as the summary symbol
%                   (prevails over all other line options except
%                   noline) 
% 
% The format of options is [<opt1>,...,<optM>]; it is correct to have
% empty options. Options are parsed left-to-right: in case of
% conflicting options, the latest prevails.
%
% If present, the rule name is typeset in text style, while the
% conclusion and the assumptions are typeset in display math mode.
% The result is a box with the correct height and width, whose
% conclusion is aligned with the current baseline.
%
% Notice that the conclusion must be present, while the assumptions
% may be absent.
%
% If there are no assumptions, i.e., if the proof tree represents an
% axiom, you may use the following commands:
%  \prfaxiom{<axiom>}
%  \prfbyaxiom{<label>}{<axiom>}
% the latter includes also the axiom name.
%
% A pure assumption is just a proof tree composed by the conclusion
% only. It uses an option to suppress the drawing of the proof line.
% The commands are:
%   \prfassumption<reference>{<formula>}
%   \prfboundedassumption<reference>{<formula>}
% the second command discharges the assumption.
%
% A proof summary is just a proof tree whose proof line is bizarre. It
% uses an option to specify the type of summary.
% The command is:
%   \prfsummary<reference>[<label>]
%              {<assumption1>}...{<assumptionN>} 
%              {<conclusion>}
% The label is optional. The shape of the summary is controlled by the
% global option \prfsummarystyle.
%
% The <reference> field above is used for labelling and
% referencing, as explained in the documentation.
%--------------------------------------------------------------------

%--------------------------------------------------------------------
% Parameters
% These values can be safely used to configure the behaviour of the
% macros in the package. Beware to modify them only outside a proof
% tree as the order in which a proof tree is typeset may vary in
% future version of the package.
%--------------------------------------------------------------------

% \prflinepad                default 0.3ex
% the space between the baseline of assumptions and the proof line and
% also the space between the proof line and the top of the conclusion
\newdimen\prflinepad\prflinepad.3ex

% \prflineextra              default 0.3em 
% the length which extends on the left and on the right the proof line
% so that it is slightly longer than the largest between the
% conclusion and the list of (direct) assumptions
\newdimen\prflineextra\prflineextra.3em

% \prflinethickness          default 0.2pt
% the thickness of the proof line
\newdimen\prflinethickness\prflinethickness.2pt

% \prfemptylinethickness     default 4 times the linethickness
% the thickness of the proof line which has to be drawn but it is empty
\newdimen\prfemptylinethickness\prfemptylinethickness4\prflinethickness

% \prfrulenameskip           default 0.2em
% the space between the proof line and the rule name
\newdimen\prfrulenameskip\prfrulenameskip.2em

% \prflabelskip           default 0.2em
% the space between the label and the proof line
\newdimen\prflabelskip\prflabelskip.2em

% \prfinterspace             default .6em
% the space between two subsequent assumptions
\newdimen\prfinterspace\prfinterspace.6em

% \prfdoublelineinterspace   default 1.2pt
% the space between a double line
\newdimen\prfdoublelineinterspace\prfdoublelineinterspace1.2pt

% \prfboundedstyle           default 0
% defines the style of bounded (discharged) assumptions:
% 0 = [<formula>]
% 1 = <formula> cancelled by a horizontal line
% >1 = uses the custom \prfdiscargedassumption command
\newcount\prfboundedstyle\prfboundedstyle0

% \prfsummarystyle           default 0
% defines the style for the summary box. The argument takes the
% following values
% 0 = a vertical dotted line (default)
% 1 = a huge \Pi
% 2 = \prod
% 3 = a calligraphic D
% >3 = uses the custom \prffancysummarybox command
\newcount\prfsummarystyle\prfsummarystyle0

% \prffancyline
% the command to draw "fancy" lines
\def\prffancyline{\cleaders\hbox to .63em%
  {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill}

% \prfConclusionBox
% the command to draw the conclusion box
\def\prfConclusionBox#1{%
  \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}

% \prfAssumptionBox
% the command to draw the assumption box
\def\prfAssumptionBox#1{%
  \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}

% \prfRuleNameBox
% the command to draw the rule name box.
\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}

% \prfLabelBox
% the command to draw the label box.
\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}

% \prfdiscargedassumption
% the command to draw a discharged assumption in a custom way.
% Users may consider the cancel.sty package
\def\prfdiscargedassumption#1{\left\langle{#1}\right\rangle}

% \prffancysummarybox
% the command to draw the body of a custom summary
\newbox\prf@@fancysummarybox
\newdimen\prf@@fancysymmarylen
\def\prffancysummarybox{%
  \sbox{\prf@@fancysummarybox}{\Huge$\bigtriangledown$}%
  \prf@@fancysymmarylen\ht\prf@@fancysummarybox%
  \advance\prf@@fancysymmarylen\dp\prf@@fancysummarybox%
  \sbox{\prf@@fancysummarybox}{%
    \raisebox{.25\prf@@fancysymmarylen}[.8\prf@@fancysymmarylen]%
    [0pt]{\usebox{\prf@@fancysummarybox}}}%
  \prf@@fancysymmarylen\wd\prf@summary@label%
  \ifdim\prf@@fancysymmarylen>\z@\relax%
    \prf@@fancysymmarylen\wd\prf@@fancysummarybox%
    \wd\prf@summary@label.4em%
    \hbox to\prf@@fancysymmarylen{%
      \usebox\prf@@fancysummarybox}\kern-.4em%
      \box\prf@summary@label%
  \else\usebox\prf@@fancysummarybox\fi}

%====================================================================

%--------------------------------------------------------------------
% What follows is intended for internal use of the package.
% It shouldn't be used in documents and may vary in future versions.
%
% Notice that we use temporary registers shared with TeX & LaTeX, and
% that some registers are shared also inside the drawing procedure!
%--------------------------------------------------------------------

% Lengths
\newskip\prf@Lassum%     space between the left border of the
                   %     assumption box and the left border of the
                   %     conclusion of the first assumption;
\newskip\prf@Rassum%     space between the right border of the
                   %     assumption box and the right border of the
                   %     conclusion of the last assumption 
\skipdef\prf@assumline1%
\skipdef\prf@concline3%
\skipdef\prf@linewd5%
\skipdef\prf@lineht3%
\skipdef\prf@linedp1%
\skipdef\prf@temp7%
\skipdef\prf@tmp7%
\skipdef\prf@Aval9%

% Boxes
\newbox\prf@assumptionsbox%   Assumptions
\newbox\prf@conclusionbox%    Conclusion
\newbox\prf@rulenamebox%      Rule name
\newbox\prf@labelbox%         Label
\newbox\prf@linebox%          Proof line
\newbox\prf@summarybox%       Summary
\newbox\prf@fancybox%         To compute the fancy line

%--------------------------------------------------------------------
% Stack implementation
%--------------------------------------------------------------------
%% End-of-stack, wrapper and stack declaration 
\def\prf@eos{\noexpand\prf@eos}
\def\prf@cons{\noexpand\prf@cons}
\let\prf@stack\prf@eos

%% Pushing a value puts the (decorated) value in front
%% of the stack list
\def\prf@push#1{\expandafter\edef\expandafter\prf@stack%
  {\prf@cons{#1}\prf@stack}}

%% Top retrieves the topmost value in the stack
\def\prf@@top\prf@cons#1#2\prf@eos{#1}
\def\prf@top{\expandafter\prf@@top\prf@stack}

%% Pop discard the topmost value in the stack
\def\prf@@pop\prf@cons#1#2\prf@eos{%
  \expandafter\edef\expandafter\prf@stack{#2\prf@eos}}
\def\prf@pop{\expandafter\prf@@pop\prf@stack}

%--------------------------------------------------------------------
% Checks whether two strings are equal
% \prf@streq{A}{B} if A = B then the boolean value \ifprf@same is 
% true otherwise false 
%
% There is also \prf@strlisteq{A}{L} which checks whether A is equal
% to any element in the comma-separated list L of strings
%--------------------------------------------------------------------
\newif\ifprf@same

\newcommand{\prf@streq}[2]{%
  \global\prf@samefalse\begingroup\def\1{#1}\def\2{#2}%
  \ifx\1\2\global\prf@sametrue\fi\endgroup}

\def\prf@strlisteq#1#2{\prf@@strlisteq{#1}#2,@}
\def\prf@@strlisteq#1#2,{\prf@streq{#1}{#2}%
  \ifprf@same\expandafter\prf@@strlistignore%
  \else\expandafter\prf@@@strlisteq\fi{#1}}
\def\prf@@strlistignore#1@{\relax}
\def\prf@@@strlisteq#1#2{%
  \begingroup\def\1{@}\def\2{#2}%
  \ifx\1\2\prf@@@strlistignore\else\prf@hop\fi\endgroup{#1}#2}
\def\prf@hop\fi\endgroup#1#2{\fi\endgroup\prf@@strlisteq{#1}#2}
\def\prf@@@strlistignore\else\prf@hop\fi\endgroup#1@{\fi\endgroup}

% -------------------------------------------------------------------
% Labelling and referencing
% The following commands implement the reference mechanism to allow to
% label and then refer to assumptions and summaries of proofs
% -------------------------------------------------------------------

% The counter to keep track of assumptions
\newcounter{prfassumptioncounter}
\setcounter{prfassumptioncounter}{0}

% The counter to keep track of summaries
\newcounter{prfsummarycounter}
\setcounter{prfsummarycounter}{0}

% To keep track of the options
\newif\ifprf@lbl@arabic\prf@lbl@arabictrue
\newif\ifprf@lbl@roman\prf@lbl@romanfalse
\newif\ifprf@lbl@Roman\prf@lbl@Romanfalse
\newif\ifprf@lbl@alph\prf@lbl@alphfalse
\newif\ifprf@lbl@Alph\prf@lbl@Alphfalse
\newif\ifprf@lbl@fnsymbol\prf@lbl@fnsymbolfalse
\newif\ifprf@lbl@label\prf@lbl@labelfalse

% The prooftree environment is used to define the scope of the
% assumption references
\newenvironment{prooftree}%
  {\setcounter{prfassumptioncounter}{0}}%
  {\setcounter{prfassumptioncounter}{0}}

% Test whether a reference is defined
\def\ifprf@undefref<#1>{%
  \expandafter\ifx\csname prf@ref@@#1\endcsname\relax}

% Test whether a reference has been written in the .aux file
\def\ifprf@unwrittenref<#1>{%
  \expandafter\ifx\csname prf@w@ref@#1\endcsname\relax}

% Write a reference
\def\prfref<#1>{%
  \ifprf@undefref<#1>{??}%
    \PackageWarningNoLine{prooftree}{Undefined reference <#1>}%
  \else\csname prf@ref@@#1\endcsname\relax\fi} 

% Create the anchor from what stored in the .aux file
\def\prfauxlabel#1#2{%
  \ifprf@undefref<#1>%
    \expandafter\gdef\csname prf@ref@@#1\endcsname{{#2}}\fi}

% Write the newly created label in the .aux file
\def\prf@auxwrite<#1>#2{%
  \ifprf@unwrittenref<#1>%
    \protected@write\@auxout{}{\string\prfauxlabel{#1}{#2}}%
    \expandafter\gdef\csname prf@w@ref@#1\endcsname{0}\fi}

% Generate an assumption label
\def\prf@assum@lbl<#1>{\prf@generic@lbl<#1>{prfassumptioncounter}}

% Generate a summary label 
\def\prf@summary@lbl<#1>{\prf@generic@lbl<#1>{prfsummarycounter}}

% Generate a label on a given counter
\def\prf@generic@lbl<#1>#2{%
  \prf@warningtrue\stepcounter{#2}%
  \ifprf@lbl@arabic\prf@warningfalse%
    \prf@auxwrite<#1>{\arabic{#2}}\fi%
  \ifprf@lbl@roman\prf@warningfalse%
    \prf@auxwrite<#1>{\roman{#2}}\fi%
  \ifprf@lbl@Roman\prf@warningfalse%
    \prf@auxwrite<#1>{\Roman{#2}}\fi%
  \ifprf@lbl@alph\prf@warningfalse%
    \prf@auxwrite<#1>{\alph{#2}}\fi%
  \ifprf@lbl@Alph\prf@warningfalse%
    \prf@auxwrite<#1>{\Alph{#2}}\fi%
  \ifprf@lbl@fnsymbol\prf@warningfalse%
    \prf@auxwrite<#1>{\fnsymbol{#2}}\fi%
  \ifprf@warning\prf@auxwrite<#1>{\arabic{#2}}\fi}

% Parsing of the labelled assumption options
\def\prf@lblopt#1{%
  \prf@warningtrue%
  \global\prf@lbl@arabicfalse% 
  \global\prf@lbl@romanfalse% 
  \global\prf@lbl@Romanfalse%
  \global\prf@lbl@alphfalse%
  \global\prf@lbl@Alphfalse%
  \global\prf@lbl@fnsymbolfalse%
  \global\prf@lbl@labelfalse%
  \prf@strlisteq{#1}{n,number,arabic}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@arabictrue\fi%
  \prf@strlisteq{#1}{r,roman}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@romantrue\fi%
  \prf@strlisteq{#1}{R,Roman}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@Romantrue\fi%
  \prf@strlisteq{#1}{a,alph,alpha,alphabetic}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@alphtrue\fi%
  \prf@strlisteq{#1}{A,Alph,Alpha,Alphabetic}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@Alphtrue\fi
  \prf@strlisteq{#1}{f,s,function,symbol,function symbol}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@fnsymboltrue\fi%
  \prf@strlisteq{#1}{l,label}%
  \ifprf@same\prf@warningfalse\global\prf@lbl@labeltrue\fi%
  \ifprf@warning%
    \PackageWarning{prftree}{Unrecognised option #1}\fi}

% How a labelled assumption is graphically rendered
\def\prflabelledassumptionbox#1#2{%
  \setbox\prf@fancybox\hbox{${#1}$}%
  \prf@tmp\wd\prf@fancybox%
  \setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}%
  \wd\prf@fancybox\prf@tmp%
  \prf@assumption{\box\prf@fancybox}}

% How a discharged fancy labelled assumption is graphically rendered
\def\prflabelleddiscargedassumption#1#2{%
  \prflabelledassumptionbox{\left\langle{#1}\right\rangle}{#2}}

%--------------------------------------------------------------------
% \prfassumption{<formula>}
% \prfboundedassumption{<formula>}
% 
% Commands to draw a pure assumption: the former draws a pure
% assumption, while the latter draws a pure assumption which is
% discharged. The way to mark discharging is controlled by the global
% option \prfboundedstyle
%--------------------------------------------------------------------
\def\prfassumption{\@ifnextchar<{\prf@assum@one}{\prf@assumption}}
\def\prf@assum@one<#1>{\global\prf@lbl@labelfalse\prf@assum@two#1>}
\def\prf@assum@two{\@ifnextchar[{\prf@assum@three}{\prf@assum@four}}
\def\prf@assum@three[#1]{\prf@lblopt{#1}\prf@assum@four}
\def\prf@assum@four#1>#2{%
  \ifprf@unwrittenref<#1>\relax%
  \else\ifprf@lbl@label\relax\else%
    \global\prf@lbl@labeltrue%
    \PackageWarningNoLine{prftree}{Label <#1> is [label]!}\fi\fi%
  \ifprf@lbl@label\relax\else\prf@assum@lbl<#1>\fi%
  \prflabelledassumptionbox{#2}{\prfref<#1>}}
\def\prf@assumption#1{\prftree[noline]{#1}\relax}

\def\prfboundedassumption{%
  \@ifnextchar<{\prf@bassum@one}{\prf@boundedassumption}}
\def\prf@bassum@one<#1>{\global\prf@lbl@labelfalse\prf@bassum@two#1>}
\def\prf@bassum@two{\@ifnextchar[{\prf@bassum@three}{\prf@bassum@four}}
\def\prf@bassum@three[#1]{\prf@lblopt{#1}\prf@bassum@four}
\def\prf@bassum@four#1>#2{%
  \ifprf@unwrittenref<#1>\relax%
  \else\ifprf@lbl@label\relax\else%
    \global\prf@lbl@labeltrue%
    \PackageWarningNoLine{prftree}{Label <#1> is [label]!}\fi\fi%
  \ifprf@lbl@label\relax\else\prf@assum@lbl<#1>\fi%
  \prftree[noline]{\prf@labelledbounded{#2}{#1}}\relax}
\def\prf@boundedassumption#1{\prftree[noline]{\prf@bounded{#1}}\relax}
\def\prf@bounded#1{%
  \ifnum\prfboundedstyle=0\left[{#1}\right]%
  \else\ifnum\prfboundedstyle=1%
      \setbox\prf@conclusionbox\prfConclusionBox{#1}%
      \prf@tmp\wd\prf@conclusionbox%
      \prf@linedp.5\ht\prf@conclusionbox%
      \advance\prf@linedp-.5\dp\prf@conclusionbox%
      \prf@lineht\prf@linedp\advance\prf@lineht\prflinethickness%
      \edef\prf@cancel{\hskip-\prf@tmp%
        \vrule width\prf@tmp height\prf@lineht depth-\prf@linedp}%
      {#1}\prf@cancel%
    \else\prfdiscargedassumption{#1}\fi\fi}  
\def\prf@labelledbounded#1#2{%
  \ifnum\prfboundedstyle=0%
    \prflabelledassumptionbox{\left[{#1}\right]}{\prfref<#2>}%
  \else\ifnum\prfboundedstyle=1%
      \setbox\prf@conclusionbox\prfConclusionBox{#1}%
      \prf@tmp\wd\prf@conclusionbox%
      \prf@linedp.5\ht\prf@conclusionbox%
      \advance\prf@linedp-.5\dp\prf@conclusionbox%
      \prf@lineht\prf@linedp\advance\prf@lineht\prflinethickness%
      \edef\prf@cancel{\hskip-\prf@tmp%
        \vrule width\prf@tmp height\prf@lineht depth-\prf@linedp}%
      \prflabelledassumptionbox{{#1}\prf@cancel}{\prfref<#2>}%
    \else\prflabelleddiscargedassumption{#1}{\prfref<#2>}\fi\fi}  

%--------------------------------------------------------------------
% \prfaxiom{<axiom>}
% \prfbyaxiom{<label>}{<axiom>}
%
% Commands to draw an axiom: the former draws the axiom, while the
% latter includes also a rule name for the axiom.
%--------------------------------------------------------------------
\def\prfaxiom#1{\prftree[single,straight]{#1}\relax}
\def\prfbyaxiom#1#2{\prftree[single,straight,rule]{#1}{#2}\relax}

%--------------------------------------------------------------------
% \prfsummary[<label>]
%            {<assumption1>}...{<assumptionN>} 
%            {<conclusion>}
%
% Command to draw a proof summary, i.e., a structure with assumptions
% 1 to N and a conclusion which stands for a complex proof not
% explicited. The label is optional.
% The shape of the summary is controlled by the global option
% \prfsummarystyle 
%--------------------------------------------------------------------
\def\prfsummary{\@ifnextchar<{\prf@summary@one}{\prf@summary}}
\def\prf@summary@one<#1>{%
  \global\prf@lbl@labelfalse\prf@summary@four#1>}
\def\prf@summary@four{%
  \@ifnextchar[{\prf@summary@five}{\prf@summary@six}}
\def\prf@summary@five[#1]#2>{%
  \prf@lblopt{#1}%
  \ifprf@unwrittenref<#2>\relax%
  \else\ifprf@lbl@label\relax\else%
    \global\prf@lbl@labeltrue%
    \PackageWarningNoLine{prftree}{Label <#2> is [label]!}\fi\fi%
  \ifprf@lbl@label\relax\else\prf@summary@lbl<#2>\fi%
  \setbox\prf@summary@label\hbox{\scriptsize\prfref<#2>}%
  \prf@summary}
\def\prf@summary@six#1>{%
  \ifprf@lbl@label\relax\else\prf@summary@lbl<#1>\fi%
  \setbox\prf@summary@label\hbox{\scriptsize\prfref<#1>}%
  \prf@summary}
\def\prf@summary{\@ifnextchar[{\prf@summary@two}{\prf@summary@three}}
\def\prf@summary@two[#1]{\prftree[summary,rule]{#1}}
\def\prf@summary@three{\prftree[summary]}

\newbox\prf@summary@label
\def\prf@@summarystyle{%
  \ifnum3=\prfsummarystyle\relax%
    \setbox\prf@summarybox\hbox{$\mathcal{D}$}%
    \prf@tmp\wd\prf@summarybox%
    \setbox\prf@summarybox\hbox{$\mathcal{D}%
      \hbox{\box\prf@summary@label}\mathstrut$}%
    \wd\prf@summarybox\prf@tmp%
  \else\ifnum2=\prfsummarystyle\relax%
    \setbox\prf@summarybox\hbox{$\prod$}%
    \prf@tmp\wd\prf@summarybox%
    \setbox\prf@summarybox\hbox{$\prod\hbox{\box\prf@summary@label}$}% 
    \wd\prf@summarybox\prf@tmp%
  \else\ifnum1=\prfsummarystyle\relax%
    \setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}}%
    \prf@tmp\wd\prf@summarybox%
    \setbox\prf@summarybox\hbox{\hbox{\Huge$\Pi$}%
      \hbox{\box\prf@summary@label}}%
    \wd\prf@summarybox\prf@tmp%
  \else\ifnum0=\prfsummarystyle\relax%
    \setbox\prf@summarybox\hbox{$\cdot$}%
    \prf@tmp\wd\prf@summarybox%
    \setbox\prf@summarybox%
      \vbox to5.2ex{\cleaders\hbox{$\cdot$}\vfill}%
    \setbox\prf@summarybox\hbox{\usebox{\prf@summarybox}%
      \hbox{\ \box\prf@summary@label}}%
    \wd\prf@summarybox\prf@tmp%
  \else\setbox\prf@summarybox\hbox{\prffancysummarybox}\fi\fi\fi\fi% 
  \prf@tmp.5\ht\prf@summarybox%
  \advance\prf@tmp-.5\dp\prf@summarybox%
  \setbox\prf@summarybox%
    \hbox{\lower\prf@tmp\hbox{\box\prf@summarybox}}}%

%--------------------------------------------------------------------
% \prftree[<options>]...[<options>]
%         {<assumption1>}...{<assumptionN>}
%         {<conclusion>}
% 
% The format of options is [<opt1>,...,<optM>]; it is correct to have
% empty options. Options are parsed left-to-right: in case of
% conflicting options, the latest prevails. See the documentation for
% their description.
%
% If present, the rule name is typesetted in text style, while the
% conclusion and the assumptions are typesetted in math mode.
% The result is a box with the correct height and width, whose
% conclusion is aligned with the current baseline.
%
% Notice that the conclusion must be present, while the assumptions
% may be absent.
%
% Options and the way things are drawn can be modified via the global
% settings of the package (see above). Notice that changing these
% settings inside a proof tree may lead to impredictable results, as
% the typesetting may proceed in an arbitrary order.
%--------------------------------------------------------------------
\newif\ifprf@rule%
\newif\ifprf@label%
\newif\ifprf@noline%
\newif\ifprf@doubleline%
\newif\ifprf@straightline%
\newif\ifprf@dottedline%
\newif\ifprf@dashedline%
\newif\ifprf@fancyline%
\newif\ifprf@summary%
\newif\ifprf@first%
\newif\ifprf@warning%
\newif\ifprf@assum

% The real parsing command is \prf@Ntree; the external command sets
% the right values for the various switches controlling the options
\def\prftree{\prf@init\prf@Ntree}
\def\prf@init{%
  \global\prf@rulefalse%
  \global\prf@labelfalse%
  \global\prf@nolinefalse%
  \global\prf@doublelinefalse%
  \global\prf@straightlinetrue%
  \global\prf@dottedlinefalse%
  \global\prf@dashedlinefalse%
  \global\prf@fancylinefalse%
  \global\prf@summaryfalse}

% If there are options then parse them, eventually setting the
% booleans to their appropriate values. Then, expand \prf@@tree
\def\prf@Ntree{\@ifnextchar[{\prf@options}{\prf@@tree}}

% Parses a block [<opt>,...,<opt>] of options one by one, left to
% right 
\def\prf@options[#1]{\prf@opts#1,]\prf@Ntree}
\def\prf@opts#1,{\prf@opt#1,\@ifnextchar]{\prf@optsskip}{\prf@opts}} 
\def\prf@optsskip]{\relax} % to consume the final ]

% Parses a single option eventually setting the appropriate flag 
\def\prf@opt#1,{\prf@warningtrue%
  \prf@strlisteq{#1}{r,by rule,rule,by,right}%
  \ifprf@same\prf@warningfalse\global\prf@ruletrue\fi%
  \prf@strlisteq{#1}{l,label,left}%
  \ifprf@same\prf@warningfalse\global\prf@labeltrue\fi%
  \prf@strlisteq{#1}{s,single line,single,singleline}%
  \ifprf@same\prf@warningfalse\global\prf@doublelinefalse\fi%
  \prf@strlisteq{#1}{d,double line,double,doubleline}%
  \ifprf@same\prf@warningfalse\global\prf@doublelinetrue\fi%
  \prf@strlisteq{#1}{straight,straight line,straightline}%
  \ifprf@same\prf@warningfalse%
  \global\prf@straightlinetrue\global\prf@dottedlinefalse%
  \global\prf@dashedlinefalse\global\prf@fancylinefalse\fi%
  \prf@strlisteq{#1}{dotted,dotted line,dottedline}%
  \ifprf@same\prf@warningfalse%
  \global\prf@straightlinefalse\global\prf@dottedlinetrue%
  \global\prf@dashedlinefalse\global\prf@fancylinefalse\fi%
  \prf@strlisteq{#1}{dashed,dashed line,dashedline}%
  \ifprf@same\prf@warningfalse%
  \global\prf@straightlinefalse\global\prf@dottedlinefalse%
  \global\prf@dashedlinetrue\global\prf@fancylinefalse\fi%
  \prf@strlisteq{#1}{f,fancy line,fancy,fancyline}%
  \ifprf@same\prf@warningfalse%
  \global\prf@straightlinefalse\global\prf@dottedlinefalse%
  \global\prf@dashedlinefalse\global\prf@fancylinetrue\fi%
  \prf@strlisteq{#1}{noline}%
  \ifprf@same\prf@warningfalse\global\prf@nolinetrue\fi%
  \prf@strlisteq{#1}{summary}%
  \ifprf@same\prf@warningfalse\global\prf@summarytrue\fi%
  \ifprf@warning\PackageWarning{prftree}%
                               {Unrecognised option #1}\fi}%

% At this point, options have been parsed. So, we process them
% preparing the right parameters for the drawing procedure. 
% We start from the proof line options:
%   0 = single straight line
%   1 = double straight line 
%   2 = single dotted line
%   3 = double dotted line
%   4 = single dashed line
%   5 = double dashed line
%   6 = single fancy line
%   7 = double fancy line
%   8 = no line
%   9 = summary
\def\prf@@tree{%
  \countdef\prf@linetype1\prf@linetype0%
  \ifprf@dottedline\prf@linetype2\fi%
  \ifprf@dashedline\prf@linetype4\fi%
  \ifprf@fancyline\prf@linetype6\fi%
  \ifprf@doubleline\advance\prf@linetype1\fi%
  \ifprf@noline\prf@linetype8\fi%
  \ifprf@summary\prf@linetype9\fi\relax%
  \expandafter\prf@@Ntree\the\prf@linetype}

% If there is no rule name, we put an empty one in place 
% #1 the line options
\def\prf@@Ntree#1{%
  \edef\prf@choice{\ifprf@rule{#1}\else{#1}{}\fi}%
  \expandafter\prf@@NNtree\prf@choice}

% If there is no label, we put an empty one in place 
% #1 the line options
% #2 the rule name
\def\prf@@NNtree#1#2{%
  \edef\prf@choice{\ifprf@label{#1}{#2}\else{#1}{#2}{}\fi}%
  \expandafter\prf@tree\prf@choice}

% We collect the first assumption, if any, or the conclusion otherwise
% and we look if there is another argument. If not, we draw the proof.
% #1 the line options' value
% #2 the rule name
% #3 the label
% #4 the conclusion or the first assumption 
\def\prf@tree#1#2#3#4{\@ifnextchar\bgroup%
  {\prf@assumptions{#1}{#2}{#3}{\prf@preprf{#4}}}%
  {\prf@draw{#1}{#2}{#3}{#4}{\prf@preprf}{}}}

% We examine assumptions from left to right. If we hit the last
% argument, it is the conclusion and the proof is ready to be drawn. 
% #1 the line options' value
% #2 the rule name
% #3 the label
% #4 the first assumptions
% #5 the current argument
\def\prf@assumptions#1#2#3#4#5{\@ifnextchar\bgroup%
  {\prf@assumenext{#1}{#2}{#3}{#4}{\prf@interprf{#5}}}%
  {\prf@draw{#1}{#2}{#3}{#5}{#4}{}}}

% An intermediate assumption is added to the assumptions' box, until
% the last assumption has been collected. Then the proof is drawn.
% #1 the line options' value
% #2 the rule name
% #3 the label
% #4 the first assumption
% #5 the complete list of assumptions
% #6 the new argument
\def\prf@assumenext#1#2#3#4#5#6{\@ifnextchar\bgroup%
  {\prf@assumenext{#1}{#2}{#3}{#4}{{#5}\prf@interprf{#6}}}%
  {\prf@draw{#1}{#2}{#3}{#6}{#4}{#5}}}

% We need to reset some internal variables during the generation of
% the assumptions
\def\prf@preprf{\global\prf@Lassum\z@\global\prf@Rassum\z@}

% We need to put some space between assumptions when generating them 
\def\prf@interprf{\hskip\prfinterspace}

%--------------------------------------------------------------------
% The drawing procedure, i.e., the "core" of the package
% #1 the line options' value
% #2 the rule name
% #3 the label 
% #4 the conclusion
% #5 the first assumption
% #6 the list of assumptions
%--------------------------------------------------------------------

\def\prf@draw#1#2#3#4#5#6{%
  % We construct the boxes which will constitute the proof
  \ifprf@first\prf@push{1}\else\prf@push{0}\fi%
  \global\prf@firsttrue%
  \setbox\prf@assumptionsbox\prfAssumptionBox{#5}%
  \prf@push{\the\prf@Lassum}%
  \global\prf@firstfalse%
  \ifdim\wd\prf@assumptionsbox>\z@\relax\prf@assumtrue%
    \setbox\prf@assumptionsbox%
      \hbox{\box\prf@assumptionsbox\prfAssumptionBox{#6}}%
  \else\prf@assumfalse%
    \setbox\prf@assumptionsbox\hbox{}\fi%
  \prf@push{\the\prf@Rassum}%
  \setbox\prf@conclusionbox\prfConclusionBox{#4}%
  \setbox\prf@rulenamebox\prfRuleNameBox{#2}%
  \setbox\prf@labelbox\prfLabelBox{#3}%
  % We set up the flags needed to format the proof tree box
  \prf@nolinefalse\prf@doublelinefalse\prf@straightlinetrue%
  \prf@dottedlinefalse\prf@dashedlinefalse\prf@fancylinefalse%
  \prf@summaryfalse\prf@rulefalse\prf@labelfalse%
  \ifcase#1\relax\or%
  \prf@doublelinetrue\or%
  \prf@dottedlinetrue\prf@straightlinefalse\or%
  \prf@doublelinetrue\prf@dottedlinetrue\prf@straightlinefalse\or%
  \prf@dashedlinetrue\prf@straightlinefalse\or%
  \prf@doublelinetrue\prf@dashedlinetrue\prf@straightlinefalse\or%
  \prf@fancylinetrue\prf@straightlinefalse\or%
  \prf@doublelinetrue\prf@fancylinetrue\prf@straightlinefalse\or%
  \prf@nolinetrue\prf@straightlinefalse\or%
  \prf@summarytrue\prf@straightlinefalse\fi%
  \ifdim\wd\prf@rulenamebox>\z@\relax\prf@ruletrue%
  \else\prf@rulefalse\fi%
  \ifdim\wd\prf@labelbox>\z@\relax\prf@labeltrue%
  \else\prf@labelfalse\fi%
  \ifdim\wd\prf@assumptionsbox>\z@\relax\prf@assumtrue%
  \else\prf@assumfalse\fi%
  % Now, we retrieve the right values for Lassum and Rassum
  % since box construction may have overwritten them. Also, we need to
  % know if this proof is the first of a list of assumptions
  \edef\prf@tok{\prf@top}\prf@pop\global\prf@Rassum\prf@tok%
  \edef\prf@tok{\prf@top}\prf@pop\global\prf@Lassum\prf@tok%
  \edef\prf@tok{\prf@top}\prf@pop\global\prf@firstfalse%
  \ifnum\prf@tok=1\global\prf@firsttrue\fi%
  % The assumptions' box has the following shape
  %  --------------------------------
  % |<---------------------wd------->|
  % | -----------       ------------ |
  % ||<-->       |     |      <---->||
  % || Lassum    | ... |   Rassum   ||
  % ||   |       |     |      |     ||
  % ||   V       |     |      V     ||
  % | -----------       ------------ |
  %  --------------------------------
  % The assumptions' line is composed by the conclusions of the
  % proofs which are the antecedents of the application of the
  % inference rule
  % The final box will be something like
  %  --------------------------------
  % |<---------------------wd------->|
  % | -----------       ------------ |
  % ||<-->       |     |      <---->||
  % || Lassum    | ... |   Rassum   ||
  % ||   |       |     |      |     ||
  % ||   V       |     |      V     ||
  % | -----------       ------------ |
  %  --------------------------------
  %     ========================   rule name
  %             conclusion
  % <--Lassum-->          <-----Rassum----->
  % 
  % We calculate the length of the assumptions' line:
  %   assumline = assumptionsbox - Lassum - Rassum
  % if there are no assumption, assumline = 0
  % (for efficiency reasons, we actually calculate 1/2assumline)
  \ifprf@assum\prf@assumline.5\wd\prf@assumptionsbox%
    \advance\prf@assumline-.5\prf@Lassum%
    \advance\prf@assumline-.5\prf@Rassum%
    \else\prf@assumline\z@\fi%
  % The length of the conclusionbox
  % (for efficiency reasons, we actually calculate 1/2concline)
  \prf@concline.5\wd\prf@conclusionbox%
  % The length of the proof line is 
  %   linewd = if summary then width of summary box else
  %               max(concline,assumline)
  %   if there is a line, we add 2extra
  % (for efficiency reasons, we actually calculate 1/2linewd)
  \ifprf@summary\prf@@summarystyle\prf@linewd.5\wd\prf@summarybox%
  \else\prf@linewd\prf@assumline%
    \ifdim\prf@assumline<\prf@concline\prf@linewd\prf@concline\fi% 
    \ifprf@noline\relax\else\advance\prf@linewd\prflineextra\fi\fi%
  % We calculate the proofline without label and rule name.
  \ifprf@noline\setbox\prf@fancybox\hbox{\hskip2\prf@linewd}%
  \else\ifprf@summary\setbox\prf@fancybox\copy\prf@summarybox%
  \else\ifprf@fancyline%
      \setbox\prf@fancybox\hbox to2\prf@linewd{\prffancyline}\else%
      \ifprf@dashedline%
      \setbox\prf@fancybox%
      \hbox to2\prf@linewd{\cleaders\hbox to.5em{\hss\_\hss}\hfill}\else%
      \ifprf@dottedline%
      \setbox\prf@fancybox%
      \hbox to2\prf@linewd{\cleaders\hbox to.33em{\hss.\hss}\hfill}\else% 
   % it must be a straight line!
      \setbox\prf@fancybox\hbox{\vrule width2\prf@linewd%
        height\prflinethickness}\fi\fi\fi%
  % If the line is double, we draw it twice with enough
  % (doublelineinterspace) space between the two copies. 
    \ifprf@doubleline%
      \setbox\prf@fancybox\hbox{\vbox{\copy\prf@fancybox%
         \nointerlineskip\vskip\prfdoublelineinterspace\nointerlineskip%
         \box\prf@fancybox}}\fi\fi\fi%
  \prf@tmp\dp\prf@fancybox%
  \setbox\prf@fancybox\hbox{\raise\prf@tmp\box\prf@fancybox}%
  % Let A = max(1/2assumline + Lassum, 1/2conclusionbox, 1/2linewd +
  % delta), where delta is 0 if there is no label, and it is the width
  % of the label box plus prflabelskip otherwise.
  % Then
  %   Assumptions shift         = A - (1/2assumline + Lassum)
  %   Rule line shift           = A - (1/2linewd + delta)
  %   Lassum = Conclusion shift = A - 1/2conclusionbox
  % And, so, we can prepare the assumptions box and the conclusion box 
  \prf@Aval\prf@assumline\advance\prf@Aval\prf@Lassum%
  \prf@tmp\prf@linewd\relax%
  \ifprf@label\advance\prf@tmp\wd\prf@labelbox%
    \advance\prf@tmp\prflabelskip\fi%
  \ifdim\prf@Aval<\prf@tmp\prf@Aval\prf@tmp\fi%
  \ifdim\prf@Aval<\prf@concline\prf@Aval\prf@concline\fi%
  \prf@temp\prf@Aval\advance\prf@temp-\prf@assumline%
  \advance\prf@temp-\prf@Lassum%
  \setbox\prf@assumptionsbox%
    \hbox{\hskip\prf@temp\box\prf@assumptionsbox}%
  \prf@temp\prf@Aval\advance\prf@temp-\prf@concline%
  \setbox\prf@conclusionbox%
    \hbox{\hskip\prf@temp\box\prf@conclusionbox}%
  \global\prf@Lassum\prf@temp%
  % Rassum will be the width of the composition of all boxes (but we
  % still have to cope with heigths...) minus (concline + conclusion
  % shift) 
  \global\prf@Rassum-2\prf@concline%
  \global\advance\prf@Rassum-\prf@temp%
  % Then, if there is a rule name, the line is raised to align with
  % the centre of the rule name and the rule box gets attached to the
  % proof line box.
  \prf@linedp\z@%
  \ifprf@noline\setbox\prf@fancybox\hbox to2\prf@linewd{}\fi%
  \ifprf@rule\advance\prf@linedp.5\ht\prf@fancybox%
    \advance\prf@linedp-.5\ht\prf@rulenamebox%
    \advance\prf@linedp.5\dp\prf@rulenamebox%
    \setbox\prf@linebox%
      \hbox{\copy\prf@fancybox\hskip\prfrulenameskip%
        \raise\prf@linedp\box\prf@rulenamebox}%
  \else\setbox\prf@linebox\copy\prf@fancybox\fi%
  \setbox\prf@linebox\hbox{\raise\dp\prf@linebox\box\prf@linebox}%
  % Then, if there is a label, the line is raised to align with
  % the centre of the label and the label box gets attached to the
  % proof line box.
  \prf@linedp\z@%
  \prf@temp\prf@Aval\advance\prf@temp-\prf@linewd%
  \ifprf@label\advance\prf@linedp.5\ht\prf@linebox%
    \advance\prf@linedp-.5\ht\prf@labelbox%
    \advance\prf@linedp.5\dp\prf@labelbox%
    \advance\prf@temp-\prflabelskip%
    \advance\prf@temp-\wd\prf@labelbox%
    \setbox\prf@linebox%
      \hbox{\raise\prf@linedp\box\prf@labelbox%
        \hskip\prflabelskip\box\prf@linebox}\fi%
  \setbox\prf@linebox%
    \hbox{\hskip\prf@temp\raise\dp\prf@linebox\box\prf@linebox}%
  % We need to calculate the distance between the assumptions and the
  % proofline: if there are no assumptions, it is zero; if there are
  % assumptions but no rule name, it is \prflinepad; otherwise it is
  % \linepad plus half of the "real" line's height
  \prf@tmp\z@%
  \ifprf@assum%
    \ifprf@rule\prf@tmp-.5\ht\prf@linebox%
      \advance\prf@tmp.5\ht\prf@fancybox%
      \advance\prf@tmp.5\dp\prf@fancybox\fi\relax%
    \ifprf@label\ifprf@rule\relax\else%
      \prf@tmp-.5\ht\prf@linebox%
      \advance\prf@tmp.5\ht\prf@fancybox%
      \advance\prf@tmp.5\dp\prf@fancybox\fi\fi%
    \advance\prf@tmp\prflinepad%
    \setbox\prf@assumptionsbox%
      \vbox{\box\prf@assumptionsbox\nointerlineskip\vskip\prf@tmp}\fi%
  % We need to calculate the distance between the proofline and the
  % conclusion: it is slightly complex to explain... try to draw the
  % whole thing to make it clear!! 
  \prf@temp\prflinepad%
  \ifprf@noline%
    \ifprf@assum%
      \advance\prf@temp\prfemptylinethickness\fi%
    \advance\prf@temp-\prflinepad\fi%
  \ifprf@rule%
    \advance\prf@temp-.5\ht\prf@linebox%
    \advance\prf@temp.5\ht\prf@fancybox%
    \advance\prf@temp.5\dp\prf@fancybox\fi%
  \ifprf@label\ifprf@rule\relax\else%
    \advance\prf@temp-.5\ht\prf@linebox%
    \advance\prf@temp.5\ht\prf@fancybox%
    \advance\prf@temp.5\dp\prf@fancybox\fi\fi%
  \setbox\prf@conclusionbox%
    \vbox{\vskip\prf@temp\box\prf@conclusionbox}%
  % And, finally, at the very end, we can prepare the proof box and we
  % can calculate the right value from Rassum. At the very end, we can
  % output the result (!!)
  \setbox\prf@rulenamebox%
    \vbox{\box\prf@assumptionsbox\nointerlineskip%
      \box\prf@linebox\nointerlineskip%
      \box\prf@conclusionbox\nointerlineskip}%
  \global\advance\prf@Rassum\wd\prf@rulenamebox%
  \hbox{$\box\prf@rulenamebox$}}

% -------------------------------------------------------------------
% The following macros are used to simplify the writing of proofs in
% natural deduction, and they roughly follow the format of proofs as
% in Troelstra, Schwichtenberg "Basic Proof Theory".
% 
% Since they may conflict with other packages, they are controlled by
% options in the package. 
% -------------------------------------------------------------------

% -------------------------------------------------------------------
% Natural deduction systems
%
% Package option [ND]
% -------------------------------------------------------------------

\newbox\prf@charbox
\def\prfscript#1{\setbox\prf@charbox%
  \hbox{$\scriptstyle\mathrm{#1}$}\copy\prf@charbox}
\ifprf@NDOption%
  \def\NDA{\prfassumption}
  \def\NDD{\prfboundedassumption}
  \def\NDAL#1{\prfassumption<#1>}
  \def\NDDL#1{\prfboundedassumption<#1>}
  \def\NDP{\prftree}
  \def\NDANDI{\prftree[by]{$\scriptstyle\wedge\prfscript{I}$}}
  \def\NDANDER{\prftree[by]{%
      $\scriptstyle\wedge\prfscript{E}_{\prfscript{R}}$}} 
  \def\NDANDEL{\prftree[by]{%
      $\scriptstyle\wedge\prfscript{E}_{\prfscript{L}}$}}
  \def\NDANDE{\prftree[by]{$\scriptstyle\wedge\prfscript{E}$}}
  \ifprfIMPOption
    \def\NDIMPI{\prftree[by]{$\scriptstyle\supset\prfscript{I}$}}
    \def\NDIMPE{\prftree[by]{$\scriptstyle\supset\prfscript{E}$}}
    \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\supset%
        \prfscript{I}_{\prfref<#1>}$}}
  \else
    \def\NDIMPI{\prftree[by]{$\scriptstyle\rightarrow%
        \prfscript{I}$}}
    \def\NDIMPE{\prftree[by]{$\scriptstyle\rightarrow%
        \prfscript{E}$}}
    \def\NDIMPIL#1{%
      \prftree[by]{$\scriptstyle\rightarrow%
        \prfscript{I}_{\prfref<#1>}$}}\fi
  \def\NDORIR{\prftree[by]{$\scriptstyle\vee%
      \prfscript{I}_{\prfscript{R}}$}}
  \def\NDORIL{\prftree[by]{$\scriptstyle\vee%
      \prfscript{I}_{\prfscript{L}}$}}
  \def\NDORI{\prftree[by]{$\scriptstyle\vee\prfscript{I}$}}
  \def\NDORE{\prftree[by]{$\scriptstyle\vee\prfscript{E}$}}
  \def\NDOREL#1{\prftree[by]{$\scriptstyle\vee%
      \prfscript{I}_{\prfref<#1>}$}}
  \def\NDALLI{\prftree[by]{$\scriptstyle\forall\prfscript{I}$}}
  \def\NDALLE{\prftree[by]{$\scriptstyle\forall\prfscript{E}$}}
  \def\NDEXI{\prftree[by]{$\scriptstyle\exists\prfscript{I}$}}
  \def\NDEXE{\prftree[by]{$\scriptstyle\exists\prfscript{E}$}}
  \def\NDEXEL#1{%
    \prftree[by]{$\scriptstyle\exists\prfscript{E}_{\prfref<#1>}$}}
  \def\NDTI{\prftree[by]{$\scriptstyle\top\prfscript{I}$}}
  \def\NDFE{\prftree[by]{$\scriptstyle\bot\prfscript{E}$}}
  \def\NDLEM{\prftree[by]{$\scriptstyle\prfscript{lem}$}}
\fi

% -------------------------------------------------------------------
% Sequent systems
%
% Package option [SEQ]
% -------------------------------------------------------------------

\ifprf@SEQOption%
  \def\SEQA{\prfassumption}
  \def\SEQD{\prfboundedassumption}
  \def\SEQP{\prftree}
  \def\SEQAX{\prftree[by]{$\scriptstyle\prfscript{Ax}$}}
  \def\SEQLF{\prftree[by]{$\scriptstyle\prfscript{L}\bot$}}
  \def\SEQLW{\prftree[by]{$\scriptstyle\prfscript{LW}$}}
  \def\SEQRW{\prftree[by]{$\scriptstyle\prfscript{RW}$}}
  \def\SEQLC{\prftree[by]{$\scriptstyle\prfscript{LC}$}}
  \def\SEQRC{\prftree[by]{$\scriptstyle\prfscript{RC}$}}
  \def\SEQLAND{\prftree[by]{$\scriptstyle\prfscript{L}\wedge$}}
  \def\SEQRAND{\prftree[by]{$\scriptstyle\prfscript{R}\wedge$}}
  \def\SEQLOR{\prftree[by]{$\scriptstyle\prfscript{L}\vee$}}
  \def\SEQROR{\prftree[by]{$\scriptstyle\prfscript{R}\vee$}}
  \ifprfIMPOption
    \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}\supset$}}
    \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}\supset$}}
  \else
    \def\SEQLIMP{\prftree[by]{$\scriptstyle\prfscript{L}%
        \rightarrow$}}
    \def\SEQRIMP{\prftree[by]{$\scriptstyle\prfscript{R}%
        \rightarrow$}}
  \fi
  \def\SEQLALL{\prftree[by]{$\scriptstyle\prfscript{L}\forall$}}
  \def\SEQRALL{\prftree[by]{$\scriptstyle\prfscript{R}\forall$}}
  \def\SEQLEX{\prftree[by]{$\scriptstyle\prfscript{L}\exists$}}
  \def\SEQREX{\prftree[by]{$\scriptstyle\prfscript{R}\exists$}}
  \def\SEQCUT{\prftree[by]{$\scriptstyle\prfscript{Cut}$}}
\fi

% -------------------------------------------------------------------