%       proof.sty       (Proof Figure Macros)

%

%       version 3.0 (for both LaTeX 2.09 and LaTeX 2e)

%       Mar 6, 1997

%       Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp)

% 

% 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.

\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner

       \relax $\relax \@MathSavedtrue \fi\fi }

\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }

%       Macros

% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.

\def\@IFnextchar#1#2#3{%

  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet

    \reserved@c\@IFnch}

\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch

      \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else

          \let\reserved@d\reserved@b\fi

      \fi \reserved@d}

\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

}