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