doc-src/proof.sty
author berghofe
Fri, 02 May 1997 16:18:11 +0200
changeset 3095 20251c80be78
child 3126 feb7a5d01c1e
permissions -rw-r--r--
Version of the proof macros for LaTeX 2e
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3095
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     1
%	proof.sty	(Proof Figure Macros)
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     2
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     3
% 	version 1.0
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     4
%	October 13, 1990
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     5
% 	Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     6
% 
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     7
% This program is free software; you can redistribute it or modify
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     8
% it under the terms of the GNU General Public License as published by
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
     9
% the Free Software Foundation; either versions 1, or (at your option)
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    10
% any later version.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    11
% 
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    12
% This program is distributed in the hope that it will be useful
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    13
% but WITHOUT ANY WARRANTY; without even the implied warranty of
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    14
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    15
% GNU General Public License for more details.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    16
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    17
%	Usage:
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    18
%		In \documentstyle, specify an optional style `proof', say,
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    19
%			\documentstyle[proof]{article}.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    20
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    21
%	The following macros are available:
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    22
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    23
%	In all the following macros, all the arguments such as
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    24
%	<Lowers> and <Uppers> are processed in math mode.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    25
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    26
%	\infer<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    27
%		draws an inference.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    28
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    29
%		Use & in <Uppers> to delimit upper formulae.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    30
%		<Uppers> consists more than 0 formulae.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    31
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    32
%		\infer returns \hbox{ ... } or \vbox{ ... } and
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    33
%		sets \@LeftOffset and \@RightOffset globally.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    34
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    35
%	\infer[<Label>]<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    36
%		draws an inference labeled with <Label>.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    37
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    38
%	\infer*<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    39
%		draws a many step deduction.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    40
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    41
%	\infer*[<Label>]<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    42
%		draws a many step deduction labeled with <Label>.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    43
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    44
%	\deduce<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    45
%		draws an inference without a rule.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    46
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    47
%	\deduce[<Proof>]<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    48
%		draws a many step deduction with a proof name.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    49
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    50
%	Example:
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    51
%		If you want to write
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    52
%       	       	    B C
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    53
%		 	   -----
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    54
%		       A     D
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    55
%		      ----------
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    56
%			  E
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    57
%	use
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    58
%		\infer{E}{
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    59
%			A
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    60
%			&
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    61
%			\infer{D}{B & C}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    62
%		}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    63
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    64
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    65
%	Style Parameters
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    66
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    67
\newdimen\inferLineSkip		\inferLineSkip=2pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    68
\newdimen\inferLabelSkip	\inferLabelSkip=5pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    69
\def\inferTabSkip{\quad}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    70
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    71
%	Variables
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    72
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    73
\newdimen\@LeftOffset	% global
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    74
\newdimen\@RightOffset	% global
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    75
\newdimen\@SavedLeftOffset	% safe from users
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    76
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    77
\newdimen\UpperWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    78
\newdimen\LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    79
\newdimen\LowerHeight
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    80
\newdimen\UpperLeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    81
\newdimen\UpperRightOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    82
\newdimen\UpperCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    83
\newdimen\LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    84
\newdimen\UpperAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    85
\newdimen\RuleAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    86
\newdimen\LowerAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    87
\newdimen\RuleWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    88
\newdimen\HLabelAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    89
\newdimen\VLabelAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    90
\newdimen\WidthAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    91
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    92
\newbox\@UpperPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    93
\newbox\@LowerPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    94
\newbox\@LabelPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    95
\newbox\ResultBox
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    96
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    97
%	Flags
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    98
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
    99
\newif\if@inferRule	% whether \@infer draws a rule.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   100
\newif\if@ReturnLeftOffset	% whether \@infer returns \@LeftOffset.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   101
\newif\if@MathSaved	% whether inner math mode where \infer or
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   102
			% \deduce appears.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   103
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   104
%	Special Fonts
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   105
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   106
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   107
    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   108
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   109
%	Math Save Macros
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   110
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   111
%	\@SaveMath is called in the very begining of toplevel macros
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   112
%	which are \infer and \deduce.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   113
%	\@RestoreMath is called in the very last before toplevel macros end.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   114
%	Remark \infer and \deduce ends calling \@infer.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   115
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   116
\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   117
	\relax $\relax \@MathSavedtrue \fi\fi }
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   118
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   119
\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   120
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   121
%	Macros
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   122
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   123
\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   124
	\ifx \@tempa \@tempb #2\else #3\fi }
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   125
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   126
\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   127
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   128
\def\@inferOneStep{\@inferRuletrue
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   129
	\@ifnextchar [{\@infer}{\@infer[\@empty]}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   130
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   131
\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   132
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   133
\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   134
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   135
\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   136
	{\@inferRulefalse \@infer[\@empty]}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   137
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   138
%	\@deduce<Proof Label>[<Proof>]<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   139
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   140
\def\@deduce#1[#2]#3#4{\@inferRulefalse
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   141
	\@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   142
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   143
%	\@infer[<Label>]<Lower><Uppers>
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   144
%		If \@inferRuletrue, draws a rule and <Label> is right to
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   145
%		a rule.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   146
%		Otherwise, draws no rule and <Label> is right to <Lower>.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   147
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   148
\def\@infer[#1]#2#3{\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   149
% Get parameters
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   150
	\if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   151
	\setbox\@LabelPart=\hbox{$#1$}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   152
	\setbox\@LowerPart=\hbox{$#2$}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   153
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   154
	\global\@LeftOffset=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   155
	\setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   156
		\global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   157
		\inferTabSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   158
		\global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   159
		#3\cr}}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   160
%			Here is a little trick.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   161
%			\@ReturnLeftOffsettrue(false) influences on \infer or
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   162
%			\deduce placed in ## locally
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   163
%			because of \@SaveMath and \@RestoreMath.
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   164
	\UpperLeftOffset=\@LeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   165
	\UpperRightOffset=\@RightOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   166
% Calculate Adjustments
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   167
	\LowerWidth=\wd\@LowerPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   168
	\LowerHeight=\ht\@LowerPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   169
	\LowerCenter=0.5\LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   170
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   171
	\UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   172
	\advance\UpperWidth by -\UpperRightOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   173
	\UpperCenter=\UpperLeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   174
	\advance\UpperCenter by 0.5\UpperWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   175
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   176
	\ifdim \UpperWidth > \LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   177
		% \UpperCenter > \LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   178
	\UpperAdjust=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   179
	\RuleAdjust=\UpperLeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   180
	\LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   181
	\RuleWidth=\UpperWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   182
	\global\@LeftOffset=\LowerAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   183
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   184
	\else	% \UpperWidth <= \LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   185
	\ifdim \UpperCenter > \LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   186
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   187
	\UpperAdjust=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   188
	\RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   189
	\LowerAdjust=\RuleAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   190
	\RuleWidth=\LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   191
	\global\@LeftOffset=\LowerAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   192
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   193
	\else	% \UpperWidth <= \LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   194
		% \UpperCenter <= \LowerCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   195
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   196
	\UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   197
	\RuleAdjust=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   198
	\LowerAdjust=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   199
	\RuleWidth=\LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   200
	\global\@LeftOffset=0pt
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   201
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   202
	\fi\fi
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   203
% Make a box
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   204
	\if@inferRule
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   205
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   206
	\setbox\ResultBox=\vbox{
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   207
		\moveright \UpperAdjust \box\@UpperPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   208
		\nointerlineskip \kern\inferLineSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   209
		\moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   210
		\nointerlineskip \kern\inferLineSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   211
		\moveright \LowerAdjust \box\@LowerPart }\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   212
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   213
	\@ifEmpty{#1}{}{\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   214
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   215
	\HLabelAdjust=\wd\ResultBox	\advance\HLabelAdjust by -\RuleAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   216
	\advance\HLabelAdjust by -\RuleWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   217
	\WidthAdjust=\HLabelAdjust
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   218
	\advance\WidthAdjust by -\inferLabelSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   219
	\advance\WidthAdjust by -\wd\@LabelPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   220
	\ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   221
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   222
	\VLabelAdjust=\dp\@LabelPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   223
	\advance\VLabelAdjust by -\ht\@LabelPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   224
	\VLabelAdjust=0.5\VLabelAdjust	\advance\VLabelAdjust by \LowerHeight
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   225
	\advance\VLabelAdjust by \inferLineSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   226
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   227
	\setbox\ResultBox=\hbox{\box\ResultBox
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   228
		\kern -\HLabelAdjust \kern\inferLabelSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   229
		\raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   230
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   231
	}\relax % end @ifEmpty
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   232
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   233
	\else % \@inferRulefalse
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   234
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   235
	\setbox\ResultBox=\vbox{
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   236
		\moveright \UpperAdjust \box\@UpperPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   237
		\nointerlineskip \kern\inferLineSkip
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   238
		\moveright \LowerAdjust \hbox{\unhbox\@LowerPart
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   239
			\@ifEmpty{#1}{}{\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   240
			\kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   241
	\fi
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   242
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   243
	\global\@RightOffset=\wd\ResultBox
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   244
	\global\advance\@RightOffset by -\@LeftOffset
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   245
	\global\advance\@RightOffset by -\LowerWidth
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   246
	\if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   247
%
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   248
	\box\ResultBox
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   249
	\@RestoreMath
20251c80be78 Version of the proof macros for LaTeX 2e
berghofe
parents:
diff changeset
   250
}