\ProvidesPackage{proof}[1995/05/22]

%       proof.sty       (Proof Figure Macros)

%

%       version 2.0

%       June 24, 1991

%       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)

%

%Modified for LaTeX-2e by L. C. Paulson

% 

% This program is free software; you can redistribute it or modify

% it under the terms of the GNU General Public License as published by

% the Free Software Foundation; either versions 1, or (at your option)

% any later version.

% 

% This program is distributed in the hope that it will be useful

% but WITHOUT ANY WARRANTY; without even the implied warranty of

% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

% GNU General Public License for more details.

%

%       Usage:

%               In \documentstyle, specify an optional style `proof', say,

%                       \documentstyle[proof]{article}.

%

%       The following macros are available:

%

%       In all the following macros, all the arguments such as

%       <Lowers> and <Uppers> are processed in math mode.

%

%       \infer<Lower><Uppers>

%               draws an inference.

%

%               Use & in <Uppers> to delimit upper formulae.

%               <Uppers> consists more than 0 formulae.

%

%               \infer returns \hbox{ ... } or \vbox{ ... } and

%               sets \@LeftOffset and \@RightOffset globally.

%

%       \infer[<Label>]<Lower><Uppers>

%               draws an inference labeled with <Label>.

%

%       \infer*<Lower><Uppers>

%               draws a many step deduction.

%

%       \infer*[<Label>]<Lower><Uppers>

%               draws a many step deduction labeled with <Label>.

%

%       \infer=<Lower><Uppers>

%               draws a double-ruled deduction.

%

%       \infer=[<Label>]<Lower><Uppers>

%               draws a double-ruled deduction labeled with <Label>.

%

%       \deduce<Lower><Uppers>

%               draws an inference without a rule.

%

%       \deduce[<Proof>]<Lower><Uppers>

%               draws a many step deduction with a proof name.

%

%       Example:

%               If you want to write

%                           B C

%                          -----

%                      A     D

%                     ----------

%                         E

%       use

%               \infer{E}{

%                       A

%                       &

%                       \infer{D}{B & C}

%               }

%

%       Style Parameters

\newdimen\inferLineSkip         \inferLineSkip=2pt

\newdimen\inferLabelSkip        \inferLabelSkip=5pt

\def\inferTabSkip{\quad}

%       Variables

\newdimen\@LeftOffset   % global

\newdimen\@RightOffset  % global

\newdimen\@SavedLeftOffset      % safe from users

\newdimen\UpperWidth

\newdimen\LowerWidth

\newdimen\LowerHeight

\newdimen\UpperLeftOffset

\newdimen\UpperRightOffset

\newdimen\UpperCenter

\newdimen\LowerCenter

\newdimen\UpperAdjust

\newdimen\RuleAdjust

\newdimen\LowerAdjust

\newdimen\RuleWidth

\newdimen\HLabelAdjust

\newdimen\VLabelAdjust

\newdimen\WidthAdjust

\newbox\@UpperPart

\newbox\@LowerPart

\newbox\@LabelPart

\newbox\ResultBox

%       Flags

\newif\if@inferRule     % whether \@infer draws a rule.

\newif\if@DoubleRule    % whether \@infer draws doulbe rules.

\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.

\newif\if@MathSaved     % whether inner math mode where \infer or

                        % \deduce appears.

%       Special Fonts

\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@

    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}

%       Math Save Macros

%

%       \@SaveMath is called in the very begining of toplevel macros

%       which are \infer and \deduce.

%       \@RestoreMath is called in the very last before toplevel macros end.

%       Remark \infer and \deduce ends calling \@infer.

%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"

\def\@SaveMath{}

\def\@RestoreMath{}

%       Macros

\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax

        \ifx \@tempa \@tempb #2\else #3\fi }

\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax

        \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}

\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse

        \@ifnextchar [{\@infer}{\@infer[\@empty]}}

\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue

        \@ifnextchar [{\@infer}{\@infer[\@empty]}}

\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}

\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}

\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}

        {\@inferRulefalse \@infer[\@empty]}}

%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>

\def\@deduce#1[#2]#3#4{\@inferRulefalse

        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}

%       \@infer[<Label>]<Lower><Uppers>

%               If \@inferRuletrue, it draws a rule and <Label> is right to

%               a rule. In this case, if \@DoubleRuletrue, it draws

%               double rules.

%

%               Otherwise, draws no rule and <Label> is right to <Lower>.

\def\@infer[#1]#2#3{\relax

% Get parameters

        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi

        \setbox\@LabelPart=\hbox{$#1$}\relax

        \setbox\@LowerPart=\hbox{$#2$}\relax

%

        \global\@LeftOffset=0pt

        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax

                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&

                \inferTabSkip

                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr

                #3\cr}}\relax

%                       Here is a little trick.

%                       \@ReturnLeftOffsettrue(false) influences on \infer or

%                       \deduce placed in ## locally

%                       because of \@SaveMath and \@RestoreMath.

        \UpperLeftOffset=\@LeftOffset

        \UpperRightOffset=\@RightOffset

% Calculate Adjustments

        \LowerWidth=\wd\@LowerPart

        \LowerHeight=\ht\@LowerPart

        \LowerCenter=0.5\LowerWidth

%

        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset

        \advance\UpperWidth by -\UpperRightOffset

        \UpperCenter=\UpperLeftOffset

        \advance\UpperCenter by 0.5\UpperWidth

%

        \ifdim \UpperWidth > \LowerWidth

                % \UpperCenter > \LowerCenter

        \UpperAdjust=0pt

        \RuleAdjust=\UpperLeftOffset

        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter

        \RuleWidth=\UpperWidth

        \global\@LeftOffset=\LowerAdjust

%

        \else   % \UpperWidth <= \LowerWidth

        \ifdim \UpperCenter > \LowerCenter

%

        \UpperAdjust=0pt

        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter

        \LowerAdjust=\RuleAdjust

        \RuleWidth=\LowerWidth

        \global\@LeftOffset=\LowerAdjust

%

        \else   % \UpperWidth <= \LowerWidth

                % \UpperCenter <= \LowerCenter

%

        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter

        \RuleAdjust=0pt

        \LowerAdjust=0pt

        \RuleWidth=\LowerWidth

        \global\@LeftOffset=0pt

%

        \fi\fi

% Make a box

        \if@inferRule

%

        \setbox\ResultBox=\vbox{

                \moveright \UpperAdjust \box\@UpperPart

                \nointerlineskip \kern\inferLineSkip

                \if@DoubleRule

                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth

                        \kern 1pt\hrule width\RuleWidth}\relax

                \else

                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax

                \fi

                \nointerlineskip \kern\inferLineSkip

                \moveright \LowerAdjust \box\@LowerPart }\relax

%

        \@ifEmpty{#1}{}{\relax

%

        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust

        \advance\HLabelAdjust by -\RuleWidth

        \WidthAdjust=\HLabelAdjust

        \advance\WidthAdjust by -\inferLabelSkip

        \advance\WidthAdjust by -\wd\@LabelPart

        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi

%

        \VLabelAdjust=\dp\@LabelPart

        \advance\VLabelAdjust by -\ht\@LabelPart

        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight

        \advance\VLabelAdjust by \inferLineSkip

%

        \setbox\ResultBox=\hbox{\box\ResultBox

                \kern -\HLabelAdjust \kern\inferLabelSkip

                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax

%

        }\relax % end @ifEmpty

%

        \else % \@inferRulefalse

%

        \setbox\ResultBox=\vbox{

                \moveright \UpperAdjust \box\@UpperPart

                \nointerlineskip \kern\inferLineSkip

                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart

                        \@ifEmpty{#1}{}{\relax

                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax

        \fi

%

        \global\@RightOffset=\wd\ResultBox

        \global\advance\@RightOffset by -\@LeftOffset

        \global\advance\@RightOffset by -\LowerWidth

        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi

%

        \box\ResultBox

        \@RestoreMath

}

\endinput