%	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

 }