%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% QUICK INFERENCE RULES
%
% Keunwoo Lee's little LaTeX hacks for inference rules.  Not as fancy
% as some other packages out there (among other things, it doesn't
% generate indexes or align the rule label in any special way), but
% it's simple and robust to inclusion in most LaTeX environments.
%
% The most recent version can be obtained from:
%
% http://www.cs.washington.edu/homes/klee/code/qinfrule.sty
%
% This code is hereby released into the public domain by its author.
% It is provided AS IS, without express or implied warranties of any
% kind, etc. blah blah blah

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% EXAMPLES
%
% The standard contravariant arrow rule:
%
% \qinfrule[Sub-Arrow]
%          {s_1 \leq t_1 \andalso t_2 \leq s_2}
%          {t_1 \rightarrow t_2 \leq s_1 \rightarrow s_2}
%
% Subtyping is reflexive:
%
% \qinfax[Sub-Refl]{t \leq t}
%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% RULES
%
% Usage:
%
%  \qinfrule[label]{premises}{consequents}
%
% The label argument is optional; i.e. the following is legal
%
%  \qinfrule{premises}{consequents}
%
% This command is as bulletproof as I can make it.  You should be
% able to use it nested inside boxes, arrays, and tabulars, and you
% should be able to use line breaks and arbitrary nested math mode
% constructs in the consequent/premises.
%
\newcommand{\qinfrule}[3][]{%
  \def\rulename{#1} \begin{tabular}{@{\,\,}cl@{\,\,}}%
  \ensuremath{\begin{array}{c}#2\end{array}}\\% \cline{1-1}&%
  \ifx\rulename\empty\else%
  \raisebox{0.5em}[0em]{\scriptsize{}(\textsc{#1})}% \fi\\%
  \raisebox{0.8em}[0em]{\ensuremath{\begin{array}[t]{c}#3\end{array}}}%
  \end{tabular}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% AXIOMS
%
% Usage:
%
%  \qinfax[label]{consquents}
%
% As with \qinfrule, the label is optional.
%
\newcommand{\qinfax}[2][]{%
  \def\rulename{#1}
  \begin{tabular}{@{\,\,}cl@{\,\,}}%
    \ensuremath{\begin{array}{c}#2\end{array}}%
    &%
    \ifx\rulename\empty\else%
      \hspace{0.5em}\scriptsize{}(\textsc{#1})%
    \fi%
  \end{tabular}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% HELPER(S)

% Space between premises
\newcommand{\andalso}{\quad\quad}