%\provide {rule}
%==========================================================================
%%%% PROOFS
%----------

%%% Judgements

\let\th=\vdash

%==========================================================================
%%% To produce a derivation separated by a line...

% The syntax  is 
%
%    <command> { <hypothesis> <middle> <conclusion> } [<labeling>]
%
%%%

% Internal use
\let \midrule=\hrule
\def \openrule {\vbox \bgroup \halign \bgroup \hfil $##$\hfil \cr}
\def \closerule {\crcr\egroup\egroup}
\def \midclosure {\crcr\noalign {\vskip -0.1em}\closerule}
\let \labclosure = \midclosure
\def \middlerule {\midclosure\over\openrule}
\def \Midclosure {\crcr \noalign
    {\vskip 0.3em \midrule \vskip -0.2em}\midclosure}
\def \Middlerule {\Midclosure\over\openrule}
\def \MIDCLOSURE {\crcr \noalign
    {\vskip 0.3em \midrule \vskip 0.1em \midrule \vskip -0.2em}\midclosure}
\def \MIDDLERULE {\MIDCLOSURE\over\openrule}

% End internal use

%% <command> are...

\def \lessskip  {\lineskiplimit=.3em\lineskip= .2em plus .1em}
\def \beginrule {\displaystyle \offinterlineskip \lessskip 
    \norulelab \bgroup \openrule}
\def \endrule {\closerule \egroup \rulelab}
\def \mathrule #1{\beginrule #1\endrule}

\def\infrule#1#2{\displaystyle \offinterlineskip \lessskip
                 \norulelab
                 \frac{\openrule#1\midclosure}{\openrule#2\closerule}
                 \rulelab}


%% <middle> is

\let \mir \middlerule
\let \Mir \Middlerule
\let \MIR \MIDDLERULE
\def \setdoublerule {\let \mir \Middlerule \let \labclosure \Midclosure}
\def \settripplerule {\let \mir \MIDDLERULE \let \labclosure \MIDCLOSURE}
\let \nl  \mir
\let \NL \MIR




% Internal or personal use
\def \gluelab{\hskip .5em}
\def \namelab#1{{\rm(\name{#1})}}
\def \namelabb#1{{\rm\name{#1}}}
\let \lab = \namelab
\let \labb = \namelabb
% End of internal use

%% <Labelling> is... 
%
%            <option> anything but an opening bracket [ <label> ]
%
%                                    or
%
%                                  <nolab>
% 
% where <option> is one of the fourth

\def \rl {\gluelab \lab}
\def \rlb {\gluelab \labb}
\def \lll #1{\lab {#1}\gluelab}
\def \Rl #1{\rlap {\rl{#1}}}
\def \lll #1{\llap {\lll{#1}}}

\def \norulelab {\let \rulelab \relax}
\def \labrule #1{\labclosure \over \gdef \rulelab {#1}\openrule}

\def \rlab #1[#2]{\labrule {\rl {#2}}}
\def \Rlab #1[#2]{\labrule {\lll {#2}}}
\def \llab #1[#2]{\labrule {\Rl {#1}}}
\def \Llab #1[#2]{\labrule {\Ll {#2}}}

% ... to put the label on the left or right of the rule
% In Capitalized commands, labels will not influence the length of the line 


% A good separator for multiple hypothesis
%   \qquad  on the same line
%   \andcr  carriage return 

\let \andcr \cr


% By default the rule is '-------', but it can be turn into '======' 
% by executing \setdoublerule  before typing the  rule.  Gouping could
% be needed to prevent this side effect from escaping.

\expandafter\ifx\csname name\endcsname\relax
   \def\name#1{\hbox{\sc #1}}\else \relax \fi

\def \Mathrule #1{\beginMathrule#1\endMathrule}
\def \beginMathrule #1\nl #2\endMathrule
    {\newdimen\Ruledimen \newdimen\ruledimen
	 \setbox0=\hbox {$\displaystyle \openrule#1\closerule$}\ruledimen=\wd0
	 \setbox0=\hbox {$\displaystyle \openrule#2\closerule$}\Ruledimen=\wd0
	 \ifnum \wd0>\ruledimen
             \advance \Ruledimen by -\ruledimen
             \divide \Ruledimen by 2
           \else
             \Ruledimen=0em
         \fi
        \def \midrule
          {\vskip-0.2em
           \hbox to \ruledimen
                       {\hskip-\Ruledimen\hrulefill\hskip -\Ruledimen}}
	 \beginrule #1\MIR#2\endrule}