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