%	proof.sty	(Proof Figure Macros)

%

% 	version 1.0

%	October 13, 1990

% 	Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.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>.

%

%	\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@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

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

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

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

\def\@inferOneStep{\@inferRuletrue

	\@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, draws a rule and <Label> is right to

%		a rule.

%		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

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

		\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

}