|
34
|
1 %
|
|
|
2 \def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
|
|
|
3 % bussproofs.sty. Version 1.1
|
|
|
4 % (c) 1994,1995,1996,2004,2005,2006, 2011.
|
|
|
5 % Copyright retained by Samuel R. Buss.
|
|
|
6 %
|
|
|
7 % ==== Legal statement: ====
|
|
|
8 % This work may be distributed and/or modified under the
|
|
|
9 % conditions of the LaTeX Project Public License, either version 1.3
|
|
|
10 % of this license or (at your option) any later version.
|
|
|
11 % The latest version of this license is in
|
|
|
12 % http://www.latex-project.org/lppl.txt.
|
|
|
13 % and version 1.3 or later is part of all distributions of LaTeX
|
|
|
14 % version 2005/12/1 or later.
|
|
|
15 %
|
|
|
16 % This work has the LPPL maintenance status 'maintained'.
|
|
|
17 %
|
|
|
18 % The Current Maintainer of the work is Sam Buss.
|
|
|
19 %
|
|
|
20 % This work consists of bussproofs.sty.
|
|
|
21 % =====
|
|
|
22 % Informal summary of legal situation:
|
|
|
23 % This software may be used and distributed freely, except that
|
|
|
24 % if you make changes, you must change the file name to be different
|
|
|
25 % than bussproofs.sty to avoid compatibility problems.
|
|
|
26 % The terms of the LaTeX Public License are the legally controlling terms
|
|
|
27 % and override any contradictory terms of the "informal situation".
|
|
|
28 %
|
|
|
29 % Please report comments and bugs to sbuss@ucsd.edu.
|
|
|
30 %
|
|
|
31 % Thanks to Felix Joachimski for making changes to let these macros
|
|
|
32 % work in plain TeX in addition to LaTeX. Nothing has been done
|
|
|
33 % to see if they work in AMSTeX. The comments below mostly
|
|
|
34 % are written for LaTeX, however.
|
|
|
35 % July 2004, version 0.7
|
|
|
36 % - bug fix, right labels with descenders inserted too much space.
|
|
|
37 % Thanks to Peter Smith for finding this bug,
|
|
|
38 % see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
|
|
|
39 % March 2005, version 0.8.
|
|
|
40 % Added a default definition for \fCenter at Denis Kosygin's
|
|
|
41 % suggestion.
|
|
|
42 % September 2005, version 0.9.
|
|
|
43 % Fixed some subtle spacing problems, by adding %'s to the end of
|
|
|
44 % few lines where they were inadvertantly omitted. Thanks to
|
|
|
45 % Arnold Beckmann for finding and fixing this problem.
|
|
|
46 % April 2006, version 0.9.1. Updated comments and testbp2.tex file.
|
|
|
47 % No change to the actual macros.
|
|
|
48 % June 2006, version 1.0. The first integer numbered release.
|
|
|
49 % New feature: root of proof may now be at the bottom instead of
|
|
|
50 % at just the top. Thanks to Alex Hertel for the suggestion to implement
|
|
|
51 % this.
|
|
|
52 % June 2011, version 1.1.
|
|
|
53 % New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann
|
|
|
54 % for taking the initiative to implement these.
|
|
|
55 % Four new commands: QuaternaryInf(C) and QuinaryInf(C).
|
|
|
56 % Bug fix: \insertBetweenHyps now works for proofs with root at top and
|
|
|
57 % three or more hypotheses..
|
|
|
58
|
|
|
59 % A good exposition of how to use bussproofs.sty (version 0.9) has been written
|
|
|
60 % by Peter Smith and is available on the internet.
|
|
|
61 % The comments below also describe the features of bussproofs.sty,
|
|
|
62 % including user-modifiable parameters.
|
|
|
63
|
|
|
64 % bussproofs.sty allows the construction of proof trees in the
|
|
|
65 % style of the sequent calculus and many other proof systems
|
|
|
66 % One novel feature of these macros is they support the horizontal
|
|
|
67 % alignment according to some center point specified with the
|
|
|
68 % command \fCenter. This is the style often used in sequent
|
|
|
69 % calculus proofs.
|
|
|
70 % Proofs are specified in left-to-right traversal order.
|
|
|
71 % For example a proof
|
|
|
72 % A B
|
|
|
73 % -----
|
|
|
74 % D C
|
|
|
75 % ---------
|
|
|
76 % E
|
|
|
77 %
|
|
|
78 % if given in the order D,A,B,C,E. Each line in the proof is
|
|
|
79 % specified according to the arity of the inference which generates
|
|
|
80 % it. Thus, E would be specified with a \BinaryInf or \BinaryInfC
|
|
|
81 % command.
|
|
|
82 %
|
|
|
83 % The above proof tree could be displayed with the commands:
|
|
|
84 %
|
|
|
85 % \AxiomC{D}
|
|
|
86 % \AxiomC{A}
|
|
|
87 % \AxiomC{B}
|
|
|
88 % \BinaryInfC{C}
|
|
|
89 % \BinaryInfC{E}
|
|
|
90 % \DisplayProof
|
|
|
91 %
|
|
|
92 % Inferences in a proof may be nullary (axioms), unary, binary, or
|
|
|
93 % trinary.
|
|
|
94 %
|
|
|
95 % IMPORTANT: You must give the \DisplayProof command to make the proof
|
|
|
96 % be printed. To display a centered proof on a line by itself,
|
|
|
97 % put the proof inside \begin{center} ... \end{center}.
|
|
|
98 %
|
|
|
99 % There are two styles for specifying horizontal centering of
|
|
|
100 % lines (formulas or sequents) in a proof. One format \AxiomC{...}
|
|
|
101 % just centers the formula {...} in the usual way. The other
|
|
|
102 % format is \Axiom$...\fCenter...$. Here, the \fCenter specifies
|
|
|
103 % the center of the formula. (It is permissable for \fCenter to
|
|
|
104 % generate typeset material; in fact, I usually define it to generate
|
|
|
105 % the sequent arrow.) In unary inferences, the \fCenter
|
|
|
106 % positions will be vertically aligned in the upper and lower lines of
|
|
|
107 % the inference. Unary, Binary, Trinary inferences are specified
|
|
|
108 % with the same format as Axioms. The two styles of centering
|
|
|
109 % lines may be combined in a single proof.
|
|
|
110 %
|
|
|
111 % By using the optional \EnableBpAbbreviations command, various
|
|
|
112 % abbreviated two or three letter commands are enabled. This allows,
|
|
|
113 % in particular:
|
|
|
114 % \AX and \AXC for \Axiom and \AxiomC, (resp.),
|
|
|
115 % \DP for \DisplayProof,
|
|
|
116 % \BI and \BIC for \BinaryInf and \BinaryInfC,
|
|
|
117 % \UI and \UIC for \UnaryInf and \UnaryInfC,
|
|
|
118 % \TI and \TIC for \TrinaryInf and \TrinaryInfC,
|
|
|
119 % \LL and \RL for \LeftLabel and \RightLabel.
|
|
|
120 % See the source code below for additional abbreviations.
|
|
|
121 % The enabling of these short abbreviations is OPTIONAL, since
|
|
|
122 % there is the possibility of conflicting with names from other
|
|
|
123 % macro packages.
|
|
|
124 %
|
|
|
125 % By default, the inferences have single horizontal lines (scores)
|
|
|
126 % This can be overridden using the \doubleLine, \noLine commands.
|
|
|
127 % These two commands affect only the next inference. You can make
|
|
|
128 % make a permanent override that applies to the rest of the current
|
|
|
129 % proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine
|
|
|
130 % and \alwaysSingleLine work in the analogous way.
|
|
|
131 %
|
|
|
132 % The macros do their best to give good placements of for the
|
|
|
133 % parts of the proof. Several macros allow you to override the
|
|
|
134 % defaults. These are \insertBetweenHyps{...} which overrides
|
|
|
135 % the default spacing between hypotheses of Binary and Trinary
|
|
|
136 % inferences with {...}. And \kernHyps{...} specifies a distance
|
|
|
137 % to shift the whole block of hypotheses to the right (modifying
|
|
|
138 % the default center position.
|
|
|
139 % Other macros set the vertical placement of the whole proof.
|
|
|
140 % The default is to try to do a good job of placement for inferences
|
|
|
141 % included in text. Two other useful macros are: \bottomAlignProof
|
|
|
142 % which aligns the hbox output by \DisplayProof according to the base
|
|
|
143 % of the bottom line of the proof, and \centerAlignProof which
|
|
|
144 % does a precise center vertical alignment.
|
|
|
145 %
|
|
|
146 % Often, one wishes to place a label next to an inference, usually
|
|
|
147 % to specify the type of inference. These labels can be placed
|
|
|
148 % by using the commands \LeftLabel{...} and \RightLabel{...}
|
|
|
149 % immediately before the command which specifies the inference.
|
|
|
150 % For example, to generate
|
|
|
151 %
|
|
|
152 % A B
|
|
|
153 % --------- X
|
|
|
154 % C
|
|
|
155 %
|
|
|
156 % use the commands
|
|
|
157 % \AxiomC{A}
|
|
|
158 % \AxiomC{B}
|
|
|
159 % \RightLabel{X}
|
|
|
160 % \BinaryInfC{C}
|
|
|
161 % \DisplayProof
|
|
|
162 %
|
|
|
163 % The \DisplayProof command just displays the proof as a text
|
|
|
164 % item. This allows you to put proofs anywhere normal text
|
|
|
165 % might appear; for example, in a paragraph, in a table, in
|
|
|
166 % a tabbing environment, etc. When displaying a proof as inline text,
|
|
|
167 % you should write \DisplayProof{} (with curly brackets) so that
|
|
|
168 % LaTeX will not "eat" the white space following the \DisplayProof
|
|
|
169 % command.
|
|
|
170 % For displaying proofs in a centered display: Do not use the \[...\]
|
|
|
171 % construction (nor $$...$$). Instead use
|
|
|
172 % \begin{center} ... \DisplayProof\end{center}.
|
|
|
173 % Actually there is a better construction to use instead of the
|
|
|
174 % \begin{center}...\DisplayProof\end{center}. This is to
|
|
|
175 % write
|
|
|
176 % \begin{prooftree} ... \end{prooftree}.
|
|
|
177 % Note there is no \DisplayProof used for this: the
|
|
|
178 % \end{prooftree} automatically supplies the \DisplayProof
|
|
|
179 % command.
|
|
|
180 %
|
|
|
181 % Warning: Any commands that set line types or set vertical or
|
|
|
182 % horizontal alignment that are given AFTER the \DisplayProof
|
|
|
183 % command will affect the next proof, no matter how distant.
|
|
|
184
|
|
|
185
|
|
|
186
|
|
|
187
|
|
|
188 % Usages:
|
|
|
189 % =======
|
|
|
190 %
|
|
|
191 % \Axiom$<antecedent>\fCenter<succedent>$
|
|
|
192 %
|
|
|
193 % \AxiomC{<whole sequent or formula}
|
|
|
194 %
|
|
|
195 % Note that the use of surrounding {}'s is mandatory in \AxiomC and
|
|
|
196 % is prohibited in $\Axiom. On the other hand, the $'s are optional
|
|
|
197 % in \AxiomC and are mandatory in \Axiom. To typeset the argument
|
|
|
198 % to \AxiomC in math mode, you must use $'s (or \(...\) ).
|
|
|
199 % The same comments apply to the inference commands below.
|
|
|
200 %
|
|
|
201 % \UnaryInf$<antecendent>\fCenter<succedent>$
|
|
|
202 %
|
|
|
203 % \UnaryInfC{<whole sequent or formula>}
|
|
|
204 %
|
|
|
205 % \BinaryInf$<antecendent>\fCenter<succedent>$
|
|
|
206 %
|
|
|
207 % \BinaryInfC{<whole sequent or formula>}
|
|
|
208 %
|
|
|
209 % \TrinaryInf$<antecendent>\fCenter<succedent>$
|
|
|
210 %
|
|
|
211 % \TrinaryInfC{<whole sequent or formula>}
|
|
|
212 %
|
|
|
213 % \QuaternaryInf$<antecendent>\fCenter<succedent>$
|
|
|
214 %
|
|
|
215 % \QuaternaryInfC{<whole sequent or formula>}
|
|
|
216 %
|
|
|
217 % \QuinaryInf$<antecendent>\fCenter<succedent>$
|
|
|
218 %
|
|
|
219 % \QuinaryInfC{<whole sequent or formula>}
|
|
|
220 %
|
|
|
221 % \LeftLabel{<text>} - Puts <text> as a label to the left
|
|
|
222 % of the next inference line. (Works even if
|
|
|
223 % \noLine is used too.)
|
|
|
224 %
|
|
|
225 % \RightLabel{<text>} - Puts <text> as a label to the right of the
|
|
|
226 % next inference line. (Also works with \noLine.)
|
|
|
227 %
|
|
|
228 % \DisplayProof - outputs the whole proof tree (and finishes it).
|
|
|
229 % The proof tree is output as an hbox.
|
|
|
230 %
|
|
|
231 %
|
|
|
232 % \kernHyps{<dimen>} - Slides the upper hypotheses right distance <dimen>
|
|
|
233 % (This is similar to shifting conclusion left)
|
|
|
234 % - kernHyps works with Unary, Binary and Trinary
|
|
|
235 % inferences and with centered or uncentered sequents.
|
|
|
236 % - Negative values for <dimen> are permitted.
|
|
|
237 %
|
|
|
238 % \insertBetweenHyps{...} - {...} will be inserted between the upper
|
|
|
239 % hypotheses of a Binary or Trinary Inferences.
|
|
|
240 % It is possible to use negative horizontal space
|
|
|
241 % to push them closer together (and even overlap).
|
|
|
242 % This command affects only the next inference.
|
|
|
243 %
|
|
|
244 % \doubleLine - Makes the current (ie, next) horizontal line doubled
|
|
|
245 %
|
|
|
246 % \alwaysDoubleLine - Makes lines doubled for rest of proof
|
|
|
247 %
|
|
|
248 % \singleLine - Makes the current (ie, next) line single
|
|
|
249 %
|
|
|
250 % \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine.
|
|
|
251 %
|
|
|
252 % \noLine - Make no line at all at current (ie next) inference.
|
|
|
253 %
|
|
|
254 % \alwaysNoLine - Makes no lines for rest of proof. (Untested)
|
|
|
255 %
|
|
|
256 % \solidLine - Does solid horizontal line for current inference
|
|
|
257 %
|
|
|
258 % \dottedLine - Does dotted horizontal line for current inference
|
|
|
259 %
|
|
|
260 % \dashedLine - Does dashed horizontal line for current inference
|
|
|
261 %
|
|
|
262 % \alwaysSolidLine - Makes the indicated change in line type, permanently
|
|
|
263 % \alwaysDashedLine until end of proof or until overridden.
|
|
|
264 % \alwaysDottedLine
|
|
|
265 %
|
|
|
266 % \bottomAlignProof - Vertically align proof according to its bottom line.
|
|
|
267 % \centerAlignProof - Vertically align proof proof precisely in its center.
|
|
|
268 % \normalAlignProof - Overrides earlier bottom/center AlignProof commands.
|
|
|
269 % The default alignment will look good in most cases,
|
|
|
270 % whether the proof is displayed or is
|
|
|
271 % in-line. Other alignments may be more
|
|
|
272 % appropriate when putting proofs in tables or
|
|
|
273 % pictures, etc. For custom alignments, use
|
|
|
274 % TeX's raise commands.
|
|
|
275 %
|
|
|
276 % \rootAtTop - specifies that proofs have their root a the top. That it,
|
|
|
277 % proofs will be "upside down".
|
|
|
278 % \rootAtBottom - (default) Specifies that proofs have root at the bottom
|
|
|
279 % The \rootAtTop and \rootAtBottom commands apply *only* to the
|
|
|
280 % current proof. If you want to make them persistent, use one of
|
|
|
281 % the next two commands:
|
|
|
282 % \alwaysRootAtTop
|
|
|
283 % \alwaysRootAtBottom (default)
|
|
|
284 %
|
|
|
285
|
|
|
286 % Optional short abbreviations for commands:
|
|
|
287 \def\EnableBpAbbreviations{%
|
|
|
288 \let\AX\Axiom
|
|
|
289 \let\AXC\AxiomC
|
|
|
290 \let\UI\UnaryInf
|
|
|
291 \let\UIC\UnaryInfC
|
|
|
292 \let\BI\BinaryInf
|
|
|
293 \let\BIC\BinaryInfC
|
|
|
294 \let\TI\TrinaryInf
|
|
|
295 \let\TIC\TrinaryInfC
|
|
|
296 \let\QI\QuaternaryInf
|
|
|
297 \let\QIC\QuaternaryInfC
|
|
|
298 \let\QuI\QuinaryInf
|
|
|
299 \let\QuIC\QuinaryInfC
|
|
|
300 \let\LL\LeftLabel
|
|
|
301 \let\RL\RightLabel
|
|
|
302 \let\DP\DisplayProof
|
|
|
303 }
|
|
|
304
|
|
|
305 % Parameters which control the style of the proof trees.
|
|
|
306 % The user may wish to override these parameters locally or globally.
|
|
|
307 % BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
|
|
|
308 % future incompatibilities). Instead, you should change them in your
|
|
|
309 % TeX document right after including this style file in the
|
|
|
310 % header material of your LaTeX document.
|
|
|
311
|
|
|
312 \def\ScoreOverhang{4pt} % How much underlines extend out
|
|
|
313 \def\ScoreOverhangLeft{\ScoreOverhang}
|
|
|
314 \def\ScoreOverhangRight{\ScoreOverhang}
|
|
|
315
|
|
|
316 \def\extraVskip{2pt} % Extra space above and below lines
|
|
|
317 \def\ruleScoreFiller{\hrule} % Horizontal rule filler.
|
|
|
318 \def\dottedScoreFiller{\hbox to4pt{\hss.\hss}}
|
|
|
319 \def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}
|
|
|
320 \def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler.
|
|
|
321 \def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start.
|
|
|
322
|
|
|
323 \def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given
|
|
|
324
|
|
|
325 \def\labelSpacing{3pt} % Horizontal space separating labels and lines
|
|
|
326
|
|
|
327 \def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex}
|
|
|
328 % Space above and below a prooftree display.
|
|
|
329
|
|
|
330 \def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom
|
|
|
331 %\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down
|
|
|
332
|
|
|
333 \ifx\fCenter\undefined
|
|
|
334 \def\fCenter{\relax}
|
|
|
335 \fi
|
|
|
336
|
|
|
337 %
|
|
|
338 % End of user-modifiable parameters.
|
|
|
339 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
340
|
|
|
341 % Here are some internal paramenters and defaults. Not really intended
|
|
|
342 % to be user-modifiable.
|
|
|
343
|
|
|
344 \def\theHypSeparation{\defaultHypSeparation}
|
|
|
345 \def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler.
|
|
|
346 \def\alwaysBuildScore{\defaultBuildScore}
|
|
|
347 \def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler.
|
|
|
348 \def\buildScore{\alwaysBuildScore} %This command builds the score.
|
|
|
349 \def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses.
|
|
|
350
|
|
|
351 \def\defaultLeftLabel{}
|
|
|
352 \def\defaultRightLabel{}
|
|
|
353
|
|
|
354 \def\myTrue{Y}
|
|
|
355 \def\bottomAlignFlag{N}
|
|
|
356 \def\centerAlignFlag{N}
|
|
|
357 \def\defaultRootAtBottomFlag{Y}
|
|
|
358 \def\rootAtBottomFlag{Y}
|
|
|
359
|
|
|
360 % End of internal parameters and defaults.
|
|
|
361
|
|
|
362 \expandafter\ifx\csname newenvironment\endcsname\relax%
|
|
|
363 % If in TeX:
|
|
|
364 \message{\BPmessage}
|
|
|
365 \def\makeatletter{\catcode`\@=11\relax}
|
|
|
366 \def\makeatother{\catcode`\@=12\relax}
|
|
|
367 \makeatletter
|
|
|
368 \def\newcount{\alloc@0\count\countdef\insc@unt}
|
|
|
369 \def\newdimen{\alloc@1\dimen\dimendef\insc@unt}
|
|
|
370 \def\newskip{\alloc@2\skip\skipdef\insc@unt}
|
|
|
371 \def\newbox{\alloc@4\box\chardef\insc@unt}
|
|
|
372 \makeatother
|
|
|
373 \else
|
|
|
374 % If in LaTeX
|
|
|
375 \typeout{\BPmessage}
|
|
|
376 \newenvironment{prooftree}%
|
|
|
377 {\begin{center}\proofSkipAmount \leavevmode}%
|
|
|
378 {\DisplayProof \proofSkipAmount \end{center} }
|
|
|
379 \fi
|
|
|
380
|
|
|
381 \def\thecur#1{\csname#1\number\theLevel\endcsname}
|
|
|
382
|
|
|
383 \newcount\theLevel % This counter is the height of the stack.
|
|
|
384 \global\theLevel=0 % Initialized to zero
|
|
|
385 \newcount\myMaxLevel
|
|
|
386 \global\myMaxLevel=0
|
|
|
387 \newbox\myBoxA % Temporary storage boxes
|
|
|
388 \newbox\myBoxB
|
|
|
389 \newbox\myBoxC
|
|
|
390 \newbox\myBoxD
|
|
|
391 \newbox\myBoxLL % Boxes for the left label and the right label.
|
|
|
392 \newbox\myBoxRL
|
|
|
393 \newdimen\thisAboveSkip %Internal use: amount to skip above line
|
|
|
394 \newdimen\thisBelowSkip %Internal use: amount to skip below line
|
|
|
395 \newdimen\newScoreStart % More temporary storage.
|
|
|
396 \newdimen\newScoreEnd
|
|
|
397 \newdimen\newCenter
|
|
|
398 \newdimen\displace
|
|
|
399 \newdimen\leftLowerAmt% Amount to lower left label
|
|
|
400 \newdimen\rightLowerAmt% Amount to lower right label
|
|
|
401 \newdimen\scoreHeight% Score height
|
|
|
402 \newdimen\scoreDepth% Score Depth
|
|
|
403 \newdimen\htLbox%
|
|
|
404 \newdimen\htRbox%
|
|
|
405 \newdimen\htRRbox%
|
|
|
406 \newdimen\htRRRbox%
|
|
|
407 \newdimen\htAbox%
|
|
|
408 \newdimen\htCbox%
|
|
|
409
|
|
|
410 \setbox\myBoxLL=\hbox{\defaultLeftLabel}%
|
|
|
411 \setbox\myBoxRL=\hbox{\defaultRightLabel}%
|
|
|
412
|
|
|
413 \def\allocatemore{%
|
|
|
414 \ifnum\theLevel>\myMaxLevel%
|
|
|
415 \expandafter\newbox\curBox%
|
|
|
416 \expandafter\newdimen\curScoreStart%
|
|
|
417 \expandafter\newdimen\curCenter%
|
|
|
418 \expandafter\newdimen\curScoreEnd%
|
|
|
419 \global\advance\myMaxLevel by1%
|
|
|
420 \fi%
|
|
|
421 }
|
|
|
422
|
|
|
423 \def\prepAxiom{%
|
|
|
424 \advance\theLevel by1%
|
|
|
425 \edef\curBox{\thecur{myBox}}%
|
|
|
426 \edef\curScoreStart{\thecur{myScoreStart}}%
|
|
|
427 \edef\curCenter{\thecur{myCenter}}%
|
|
|
428 \edef\curScoreEnd{\thecur{myScoreEnd}}%
|
|
|
429 \allocatemore%
|
|
|
430 }
|
|
|
431
|
|
|
432 \def\Axiom$#1\fCenter#2${%
|
|
|
433 % Get level and correct names set.
|
|
|
434 \prepAxiom%
|
|
|
435 % Define the boxes
|
|
|
436 \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
|
|
|
437 \setbox\myBoxB=\hbox{$#2$}%
|
|
|
438 \global\setbox\curBox=%
|
|
|
439 \hbox{\hskip\ScoreOverhangLeft\relax%
|
|
|
440 \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
|
|
|
441 % Set the relevant dimensions for the boxes
|
|
|
442 \global\curScoreStart=0pt \relax
|
|
|
443 \global\curScoreEnd=\wd\curBox \relax
|
|
|
444 \global\curCenter=\wd\myBoxA \relax
|
|
|
445 \global\advance \curCenter by \ScoreOverhangLeft%
|
|
|
446 \ignorespaces
|
|
|
447 }
|
|
|
448
|
|
|
449 \def\AxiomC#1{ % Note argument not in math mode
|
|
|
450 % Get level and correct names set.
|
|
|
451 \prepAxiom%
|
|
|
452 % Define the box.
|
|
|
453 \setbox\myBoxA=\hbox{#1}%
|
|
|
454 \global\setbox\curBox =%
|
|
|
455 \hbox{\hskip\ScoreOverhangLeft\relax%
|
|
|
456 \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
|
|
|
457 % Set the relevant dimensions for the boxes
|
|
|
458 \global\curScoreStart=0pt \relax
|
|
|
459 \global\curScoreEnd=\wd\curBox \relax
|
|
|
460 \global\curCenter=.5\wd\curBox \relax
|
|
|
461 \global\advance \curCenter by \ScoreOverhangLeft%
|
|
|
462 \ignorespaces
|
|
|
463 }
|
|
|
464
|
|
|
465 \def\prepUnary{%
|
|
|
466 \ifnum \theLevel<1
|
|
|
467 \errmessage{Hypotheses missing!}
|
|
|
468 \fi%
|
|
|
469 \edef\curBox{\thecur{myBox}}%
|
|
|
470 \edef\curScoreStart{\thecur{myScoreStart}}%
|
|
|
471 \edef\curCenter{\thecur{myCenter}}%
|
|
|
472 \edef\curScoreEnd{\thecur{myScoreEnd}}%
|
|
|
473 }
|
|
|
474
|
|
|
475 \def\UnaryInf$#1\fCenter#2${%
|
|
|
476 \prepUnary%
|
|
|
477 \buildConclusion{#1}{#2}%
|
|
|
478 \joinUnary%
|
|
|
479 \resetInferenceDefaults%
|
|
|
480 \ignorespaces%
|
|
|
481 }
|
|
|
482
|
|
|
483 \def\UnaryInfC#1{
|
|
|
484 \prepUnary%
|
|
|
485 \buildConclusionC{#1}%
|
|
|
486 %Align and join the curBox and the new box into one vbox.
|
|
|
487 \joinUnary%
|
|
|
488 \resetInferenceDefaults%
|
|
|
489 \ignorespaces%
|
|
|
490 }
|
|
|
491
|
|
|
492 \def\prepBinary{%
|
|
|
493 \ifnum\theLevel<2
|
|
|
494 \errmessage{Hypotheses missing!}
|
|
|
495 \fi%
|
|
|
496 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
|
|
|
497 \edef\rcurScoreStart{\thecur{myScoreStart}}%
|
|
|
498 \edef\rcurCenter{\thecur{myCenter}}%
|
|
|
499 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
500 \advance\theLevel by-1%
|
|
|
501 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
|
|
|
502 \edef\lcurScoreStart{\thecur{myScoreStart}}%
|
|
|
503 \edef\lcurCenter{\thecur{myCenter}}%
|
|
|
504 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
505 }
|
|
|
506
|
|
|
507 \def\BinaryInf$#1\fCenter#2${%
|
|
|
508 \prepBinary%
|
|
|
509 \buildConclusion{#1}{#2}%
|
|
|
510 \joinBinary%
|
|
|
511 \resetInferenceDefaults%
|
|
|
512 \ignorespaces%
|
|
|
513 }
|
|
|
514
|
|
|
515 \def\BinaryInfC#1{%
|
|
|
516 \prepBinary%
|
|
|
517 \buildConclusionC{#1}%
|
|
|
518 \joinBinary%
|
|
|
519 \resetInferenceDefaults%
|
|
|
520 \ignorespaces%
|
|
|
521 }
|
|
|
522
|
|
|
523 \def\prepTrinary{%
|
|
|
524 \ifnum\theLevel<3
|
|
|
525 \errmessage{Hypotheses missing!}
|
|
|
526 \fi%
|
|
|
527 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
|
|
|
528 \edef\rcurScoreStart{\thecur{myScoreStart}}%
|
|
|
529 \edef\rcurCenter{\thecur{myCenter}}%
|
|
|
530 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
531 \advance\theLevel by-1%
|
|
|
532 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
|
|
|
533 \edef\ccurScoreStart{\thecur{myScoreStart}}%
|
|
|
534 \edef\ccurCenter{\thecur{myCenter}}%
|
|
|
535 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
536 \advance\theLevel by-1%
|
|
|
537 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
|
|
|
538 \edef\lcurScoreStart{\thecur{myScoreStart}}%
|
|
|
539 \edef\lcurCenter{\thecur{myCenter}}%
|
|
|
540 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
541 }
|
|
|
542
|
|
|
543 \def\TrinaryInf$#1\fCenter#2${%
|
|
|
544 \prepTrinary%
|
|
|
545 \buildConclusion{#1}{#2}%
|
|
|
546 \joinTrinary%
|
|
|
547 \resetInferenceDefaults%
|
|
|
548 \ignorespaces%
|
|
|
549 }
|
|
|
550
|
|
|
551 \def\TrinaryInfC#1{%
|
|
|
552 \prepTrinary%
|
|
|
553 \buildConclusionC{#1}%
|
|
|
554 \joinTrinary%
|
|
|
555 \resetInferenceDefaults%
|
|
|
556 \ignorespaces%
|
|
|
557 }
|
|
|
558
|
|
|
559 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
560 \def\prepQuaternary{%
|
|
|
561 \ifnum\theLevel<4
|
|
|
562 \errmessage{Hypotheses missing!}
|
|
|
563 \fi%
|
|
|
564 \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
|
|
|
565 \edef\rrcurScoreStart{\thecur{myScoreStart}}%
|
|
|
566 \edef\rrcurCenter{\thecur{myCenter}}%
|
|
|
567 \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
568 \advance\theLevel by-1%
|
|
|
569 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
|
|
|
570 \edef\rcurScoreStart{\thecur{myScoreStart}}%
|
|
|
571 \edef\rcurCenter{\thecur{myCenter}}%
|
|
|
572 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
573 \advance\theLevel by-1%
|
|
|
574 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
|
|
|
575 \edef\ccurScoreStart{\thecur{myScoreStart}}%
|
|
|
576 \edef\ccurCenter{\thecur{myCenter}}%
|
|
|
577 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
578 \advance\theLevel by-1%
|
|
|
579 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
|
|
|
580 \edef\lcurScoreStart{\thecur{myScoreStart}}%
|
|
|
581 \edef\lcurCenter{\thecur{myCenter}}%
|
|
|
582 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
583 }
|
|
|
584
|
|
|
585 \def\QuaternaryInf$#1\fCenter#2${%
|
|
|
586 \prepQuaternary%
|
|
|
587 \buildConclusion{#1}{#2}%
|
|
|
588 \joinQuaternary%
|
|
|
589 \resetInferenceDefaults%
|
|
|
590 \ignorespaces%
|
|
|
591 }
|
|
|
592
|
|
|
593 \def\QuaternaryInfC#1{%
|
|
|
594 \prepQuaternary%
|
|
|
595 \buildConclusionC{#1}%
|
|
|
596 \joinQuaternary%
|
|
|
597 \resetInferenceDefaults%
|
|
|
598 \ignorespaces%
|
|
|
599 }
|
|
|
600
|
|
|
601 \def\joinQuaternary{% Construct the quarterary inference into a vbox.
|
|
|
602 % Join the four hypotheses's boxes into one hbox.
|
|
|
603 \setbox\myBoxA=\hbox{\theHypSeparation}%
|
|
|
604 \lcurScoreEnd=\rrcurScoreEnd%
|
|
|
605 \advance\lcurScoreEnd by\wd\rcurBox%
|
|
|
606 \advance\lcurScoreEnd by\wd\lcurBox%
|
|
|
607 \advance\lcurScoreEnd by\wd\ccurBox%
|
|
|
608 \advance\lcurScoreEnd by3\wd\myBoxA%
|
|
|
609 \displace=\lcurScoreEnd%
|
|
|
610 \advance\displace by -\lcurScoreStart%
|
|
|
611 \lcurCenter=.5\displace%
|
|
|
612 \advance\lcurCenter by\lcurScoreStart%
|
|
|
613 \ifx\rootAtBottomFlag\myTrue%
|
|
|
614 \setbox\lcurBox=%
|
|
|
615 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
|
|
|
616 \unhcopy\myBoxA\box\rcurBox
|
|
|
617 \unhcopy\myBoxA\box\rrcurBox}%
|
|
|
618 \else%
|
|
|
619 \htLbox = \ht\lcurBox%
|
|
|
620 \htAbox = \ht\myBoxA%
|
|
|
621 \htCbox = \ht\ccurBox%
|
|
|
622 \htRbox = \ht\rcurBox%
|
|
|
623 \htRRbox = \ht\rrcurBox%
|
|
|
624 \setbox\lcurBox=%
|
|
|
625 \hbox{\lower\htLbox\box\lcurBox%
|
|
|
626 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
|
|
|
627 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
|
|
|
628 \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
|
|
|
629 \fi%
|
|
|
630 % Adjust center of upper hypotheses according to how much
|
|
|
631 % the lower sequent is off-center.
|
|
|
632 \displace=\newCenter%
|
|
|
633 \advance\displace by -.5\newScoreStart%
|
|
|
634 \advance\displace by -.5\newScoreEnd%
|
|
|
635 \advance\lcurCenter by \displace%
|
|
|
636 %Align and join the curBox and the two hypotheses's box into one vbox.
|
|
|
637 \edef\curBox{\lcurBox}%
|
|
|
638 \edef\curScoreStart{\lcurScoreStart}%
|
|
|
639 \edef\curScoreEnd{\lcurScoreEnd}%
|
|
|
640 \edef\curCenter{\lcurCenter}%
|
|
|
641 \joinUnary%
|
|
|
642 }
|
|
|
643
|
|
|
644 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
645 \def\prepQuinary{%
|
|
|
646 \ifnum\theLevel<5
|
|
|
647 \errmessage{Hypotheses missing!}
|
|
|
648 \fi%
|
|
|
649 \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis
|
|
|
650 \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
|
|
|
651 \edef\rrrcurCenter{\thecur{myCenter}}%
|
|
|
652 \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
653 \advance\theLevel by-1%
|
|
|
654 \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
|
|
|
655 \edef\rrcurScoreStart{\thecur{myScoreStart}}%
|
|
|
656 \edef\rrcurCenter{\thecur{myCenter}}%
|
|
|
657 \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
658 \advance\theLevel by-1%
|
|
|
659 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
|
|
|
660 \edef\rcurScoreStart{\thecur{myScoreStart}}%
|
|
|
661 \edef\rcurCenter{\thecur{myCenter}}%
|
|
|
662 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
663 \advance\theLevel by-1%
|
|
|
664 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
|
|
|
665 \edef\ccurScoreStart{\thecur{myScoreStart}}%
|
|
|
666 \edef\ccurCenter{\thecur{myCenter}}%
|
|
|
667 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
668 \advance\theLevel by-1%
|
|
|
669 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
|
|
|
670 \edef\lcurScoreStart{\thecur{myScoreStart}}%
|
|
|
671 \edef\lcurCenter{\thecur{myCenter}}%
|
|
|
672 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
|
|
|
673 }
|
|
|
674
|
|
|
675 \def\QuinaryInf$#1\fCenter#2${%
|
|
|
676 \prepQuinary%
|
|
|
677 \buildConclusion{#1}{#2}%
|
|
|
678 \joinQuinary%
|
|
|
679 \resetInferenceDefaults%
|
|
|
680 \ignorespaces%
|
|
|
681 }
|
|
|
682
|
|
|
683 \def\QuinaryInfC#1{%
|
|
|
684 \prepQuinary%
|
|
|
685 \buildConclusionC{#1}%
|
|
|
686 \joinQuinary%
|
|
|
687 \resetInferenceDefaults%
|
|
|
688 \ignorespaces%
|
|
|
689 }
|
|
|
690
|
|
|
691 \def\joinQuinary{% Construct the quinary inference into a vbox.
|
|
|
692 % Join the five hypotheses's boxes into one hbox.
|
|
|
693 \setbox\myBoxA=\hbox{\theHypSeparation}%
|
|
|
694 \lcurScoreEnd=\rrrcurScoreEnd%
|
|
|
695 \advance\lcurScoreEnd by\wd\rrcurBox%
|
|
|
696 \advance\lcurScoreEnd by\wd\rcurBox%
|
|
|
697 \advance\lcurScoreEnd by\wd\lcurBox%
|
|
|
698 \advance\lcurScoreEnd by\wd\ccurBox%
|
|
|
699 \advance\lcurScoreEnd by4\wd\myBoxA%
|
|
|
700 \displace=\lcurScoreEnd%
|
|
|
701 \advance\displace by -\lcurScoreStart%
|
|
|
702 \lcurCenter=.5\displace%
|
|
|
703 \advance\lcurCenter by\lcurScoreStart%
|
|
|
704 \ifx\rootAtBottomFlag\myTrue%
|
|
|
705 \setbox\lcurBox=%
|
|
|
706 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
|
|
|
707 \unhcopy\myBoxA\box\rcurBox
|
|
|
708 \unhcopy\myBoxA\box\rrcurBox
|
|
|
709 \unhcopy\myBoxA\box\rrrcurBox}%
|
|
|
710 \else%
|
|
|
711 \htLbox = \ht\lcurBox%
|
|
|
712 \htAbox = \ht\myBoxA%
|
|
|
713 \htCbox = \ht\ccurBox%
|
|
|
714 \htRbox = \ht\rcurBox%
|
|
|
715 \htRRbox = \ht\rrcurBox%
|
|
|
716 \htRRRbox = \ht\rrrcurBox%
|
|
|
717 \setbox\lcurBox=%
|
|
|
718 \hbox{\lower\htLbox\box\lcurBox%
|
|
|
719 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
|
|
|
720 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
|
|
|
721 \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
|
|
|
722 \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
|
|
|
723 \fi%
|
|
|
724 % Adjust center of upper hypotheses according to how much
|
|
|
725 % the lower sequent is off-center.
|
|
|
726 \displace=\newCenter%
|
|
|
727 \advance\displace by -.5\newScoreStart%
|
|
|
728 \advance\displace by -.5\newScoreEnd%
|
|
|
729 \advance\lcurCenter by \displace%
|
|
|
730 %Align and join the curBox and the two hypotheses's box into one vbox.
|
|
|
731 \edef\curBox{\lcurBox}%
|
|
|
732 \edef\curScoreStart{\lcurScoreStart}%
|
|
|
733 \edef\curScoreEnd{\lcurScoreEnd}%
|
|
|
734 \edef\curCenter{\lcurCenter}%
|
|
|
735 \joinUnary%
|
|
|
736 }
|
|
|
737
|
|
|
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
739
|
|
|
740 \def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
|
|
|
741 % Define the boxes
|
|
|
742 \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
|
|
|
743 \setbox\myBoxB=\hbox{$#2$}%
|
|
|
744 % Put them together in \myBoxC
|
|
|
745 \setbox\myBoxC =%
|
|
|
746 \hbox{\hskip\ScoreOverhangLeft\relax%
|
|
|
747 \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
|
|
|
748 % Calculate the center of the \myBoxC string.
|
|
|
749 \newScoreStart=0pt \relax%
|
|
|
750 \newCenter=\wd\myBoxA \relax%
|
|
|
751 \advance \newCenter by \ScoreOverhangLeft%
|
|
|
752 \newScoreEnd=\wd\myBoxC%
|
|
|
753 }
|
|
|
754
|
|
|
755 \def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
|
|
|
756 % Define the box.
|
|
|
757 \setbox\myBoxA=\hbox{#1}%
|
|
|
758 \setbox\myBoxC =%
|
|
|
759 \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
|
|
|
760 \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
|
|
|
761 % Calculate kerning to line up centers
|
|
|
762 \newScoreStart=0pt \relax%
|
|
|
763 \newCenter=.5\wd\myBoxC \relax%
|
|
|
764 \newScoreEnd=\wd\myBoxC%
|
|
|
765 \advance \newCenter by \ScoreOverhangLeft%
|
|
|
766 }
|
|
|
767
|
|
|
768 \def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox
|
|
|
769 \global\advance\curCenter by -\hypKernAmt%
|
|
|
770 \ifnum\curCenter<\newCenter%
|
|
|
771 \displace=\newCenter%
|
|
|
772 \advance \displace by -\curCenter%
|
|
|
773 \kernUpperBox%
|
|
|
774 \else%
|
|
|
775 \displace=\curCenter%
|
|
|
776 \advance \displace by -\newCenter%
|
|
|
777 \kernLowerBox%
|
|
|
778 \fi%
|
|
|
779 \ifnum \newScoreStart < \curScoreStart %
|
|
|
780 \global \curScoreStart = \newScoreStart \fi%
|
|
|
781 \ifnum \curScoreEnd < \newScoreEnd %
|
|
|
782 \global \curScoreEnd = \newScoreEnd \fi%
|
|
|
783 % Leave room for the left label.
|
|
|
784 \ifnum \curScoreStart<\wd\myBoxLL%
|
|
|
785 \global\displace = \wd\myBoxLL%
|
|
|
786 \global\advance\displace by -\curScoreStart%
|
|
|
787 \kernUpperBox%
|
|
|
788 \kernLowerBox%
|
|
|
789 \fi%
|
|
|
790 % Draw the score
|
|
|
791 \buildScore%
|
|
|
792 % Form the score and labels into a box.
|
|
|
793 \buildScoreLabels%
|
|
|
794 % Form the new box and its dimensions
|
|
|
795 \ifx\rootAtBottomFlag\myTrue%
|
|
|
796 \buildRootBottom%
|
|
|
797 \else%
|
|
|
798 \buildRootTop%
|
|
|
799 \fi%
|
|
|
800 \global \curScoreStart=\newScoreStart%
|
|
|
801 \global \curScoreEnd=\newScoreEnd%
|
|
|
802 \global \curCenter=\newCenter%
|
|
|
803 }
|
|
|
804
|
|
|
805 \def\buildRootBottom{%
|
|
|
806 \global \setbox \curBox =%
|
|
|
807 \vbox{\box\curBox%
|
|
|
808 \vskip\thisAboveSkip \relax%
|
|
|
809 \nointerlineskip\box\myBoxD%
|
|
|
810 \vskip\thisBelowSkip \relax%
|
|
|
811 \nointerlineskip\box\myBoxC}%
|
|
|
812 }
|
|
|
813
|
|
|
814 \def\buildRootTop{%
|
|
|
815 \global \setbox \curBox =%
|
|
|
816 \vbox{\box\myBoxC%
|
|
|
817 \vskip\thisAboveSkip \relax%
|
|
|
818 \nointerlineskip\box\myBoxD%
|
|
|
819 \vskip\thisBelowSkip \relax%
|
|
|
820 \nointerlineskip\box\curBox}%
|
|
|
821 }
|
|
|
822
|
|
|
823 \def\kernUpperBox{%
|
|
|
824 \global\setbox\curBox =%
|
|
|
825 \hbox{\hskip\displace\box\curBox}%
|
|
|
826 \global\advance \curScoreStart by \displace%
|
|
|
827 \global\advance \curScoreEnd by \displace%
|
|
|
828 \global\advance\curCenter by \displace%
|
|
|
829 }
|
|
|
830
|
|
|
831 \def\kernLowerBox{%
|
|
|
832 \global\setbox\myBoxC =%
|
|
|
833 \hbox{\hskip\displace\unhbox\myBoxC}%
|
|
|
834 \global\advance \newScoreStart by \displace%
|
|
|
835 \global\advance \newScoreEnd by \displace%
|
|
|
836 \global\advance\newCenter by \displace%
|
|
|
837 }
|
|
|
838
|
|
|
839 \def\joinBinary{% Construct the binary inference into a vbox.
|
|
|
840 % Join the two hypotheses's boxes into one hbox.
|
|
|
841 \setbox\myBoxA=\hbox{\theHypSeparation}%
|
|
|
842 \lcurScoreEnd=\rcurScoreEnd%
|
|
|
843 \advance\lcurScoreEnd by\wd\lcurBox%
|
|
|
844 \advance\lcurScoreEnd by\wd\myBoxA%
|
|
|
845 \displace=\lcurScoreEnd%
|
|
|
846 \advance\displace by -\lcurScoreStart%
|
|
|
847 \lcurCenter=.5\displace%
|
|
|
848 \advance\lcurCenter by\lcurScoreStart%
|
|
|
849 \ifx\rootAtBottomFlag\myTrue%
|
|
|
850 \setbox\lcurBox=%
|
|
|
851 \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}%
|
|
|
852 \else%
|
|
|
853 \htLbox = \ht\lcurBox%
|
|
|
854 \htAbox = \ht\myBoxA%
|
|
|
855 \htRbox = \ht\rcurBox%
|
|
|
856 \setbox\lcurBox=%
|
|
|
857 \hbox{\lower\htLbox\box\lcurBox%
|
|
|
858 \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
|
|
|
859 \fi%
|
|
|
860 % Adjust center of upper hypotheses according to how much
|
|
|
861 % the lower sequent is off-center.
|
|
|
862 \displace=\newCenter%
|
|
|
863 \advance\displace by -.5\newScoreStart%
|
|
|
864 \advance\displace by -.5\newScoreEnd%
|
|
|
865 \advance\lcurCenter by \displace%
|
|
|
866 %Align and join the curBox and the two hypotheses's box into one vbox.
|
|
|
867 \edef\curBox{\lcurBox}%
|
|
|
868 \edef\curScoreStart{\lcurScoreStart}%
|
|
|
869 \edef\curScoreEnd{\lcurScoreEnd}%
|
|
|
870 \edef\curCenter{\lcurCenter}%
|
|
|
871 \joinUnary%
|
|
|
872 }
|
|
|
873
|
|
|
874 \def\joinTrinary{% Construct the trinary inference into a vbox.
|
|
|
875 % Join the three hypotheses's boxes into one hbox.
|
|
|
876 \setbox\myBoxA=\hbox{\theHypSeparation}%
|
|
|
877 \lcurScoreEnd=\rcurScoreEnd%
|
|
|
878 \advance\lcurScoreEnd by\wd\lcurBox%
|
|
|
879 \advance\lcurScoreEnd by\wd\ccurBox%
|
|
|
880 \advance\lcurScoreEnd by2\wd\myBoxA%
|
|
|
881 \displace=\lcurScoreEnd%
|
|
|
882 \advance\displace by -\lcurScoreStart%
|
|
|
883 \lcurCenter=.5\displace%
|
|
|
884 \advance\lcurCenter by\lcurScoreStart%
|
|
|
885 \ifx\rootAtBottomFlag\myTrue%
|
|
|
886 \setbox\lcurBox=%
|
|
|
887 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
|
|
|
888 \unhcopy\myBoxA\box\rcurBox}%
|
|
|
889 \else%
|
|
|
890 \htLbox = \ht\lcurBox%
|
|
|
891 \htAbox = \ht\myBoxA%
|
|
|
892 \htCbox = \ht\ccurBox%
|
|
|
893 \htRbox = \ht\rcurBox%
|
|
|
894 \setbox\lcurBox=%
|
|
|
895 \hbox{\lower\htLbox\box\lcurBox%
|
|
|
896 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
|
|
|
897 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
|
|
|
898 \fi%
|
|
|
899 % Adjust center of upper hypotheses according to how much
|
|
|
900 % the lower sequent is off-center.
|
|
|
901 \displace=\newCenter%
|
|
|
902 \advance\displace by -.5\newScoreStart%
|
|
|
903 \advance\displace by -.5\newScoreEnd%
|
|
|
904 \advance\lcurCenter by \displace%
|
|
|
905 %Align and join the curBox and the two hypotheses's box into one vbox.
|
|
|
906 \edef\curBox{\lcurBox}%
|
|
|
907 \edef\curScoreStart{\lcurScoreStart}%
|
|
|
908 \edef\curScoreEnd{\lcurScoreEnd}%
|
|
|
909 \edef\curCenter{\lcurCenter}%
|
|
|
910 \joinUnary%
|
|
|
911 }
|
|
|
912
|
|
|
913 \def\DisplayProof{%
|
|
|
914 % Display (and purge) the proof tree.
|
|
|
915 % Choose the appropriate vertical alignment.
|
|
|
916 \ifnum \theLevel=1 \relax \else%x
|
|
|
917 \errmessage{Proof tree badly specified.}%
|
|
|
918 \fi%
|
|
|
919 \edef\curBox{\thecur{myBox}}%
|
|
|
920 \ifx\bottomAlignFlag\myTrue%
|
|
|
921 \displace=0pt%
|
|
|
922 \else%
|
|
|
923 \displace=.5\ht\curBox%
|
|
|
924 \ifx\centerAlignFlag\myTrue\relax
|
|
|
925 \else%
|
|
|
926 \advance\displace by -3pt%
|
|
|
927 \fi%
|
|
|
928 \fi%
|
|
|
929 \leavevmode%
|
|
|
930 \lower\displace\hbox{\copy\curBox}%
|
|
|
931 \global\theLevel=0%
|
|
|
932 \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always"
|
|
|
933 \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always"
|
|
|
934 \global\def\bottomAlignFlag{N}%
|
|
|
935 \global\def\centerAlignFlag{N}%
|
|
|
936 \resetRootPosition
|
|
|
937 \resetInferenceDefaults%
|
|
|
938 \ignorespaces
|
|
|
939 }
|
|
|
940
|
|
|
941 \def\buildSingleScore{% Make an hbox with a single score.
|
|
|
942 \displace=\curScoreEnd%
|
|
|
943 \advance \displace by -\curScoreStart%
|
|
|
944 \global\setbox \myBoxD =%
|
|
|
945 \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}%
|
|
|
946 %\global\setbox \myBoxD =%
|
|
|
947 %\hbox{\hskip\curScoreStart\relax \box\myBoxD}%
|
|
|
948 }
|
|
|
949
|
|
|
950 \def\buildDoubleScore{% Make an hbox with a double score.
|
|
|
951 \buildSingleScore%
|
|
|
952 \global\setbox\myBoxD=%
|
|
|
953 \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}%
|
|
|
954 }
|
|
|
955
|
|
|
956 \def\buildNoScore{% Make an hbox with no score (raise a little anyway)
|
|
|
957 \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}%
|
|
|
958 }
|
|
|
959
|
|
|
960 \def\doubleLine{%
|
|
|
961 \gdef\buildScore{\buildDoubleScore}% Set next score to this type
|
|
|
962 \ignorespaces
|
|
|
963 }
|
|
|
964 \def\alwaysDoubleLine{%
|
|
|
965 \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof.
|
|
|
966 \gdef\buildScore{\buildDoubleScore}% Set next score to be double
|
|
|
967 \ignorespaces
|
|
|
968 }
|
|
|
969 \def\singleLine{%
|
|
|
970 \gdef\buildScore{\buildSingleScore}% Set next score to be single
|
|
|
971 \ignorespaces
|
|
|
972 }
|
|
|
973 \def\alwaysSingleLine{%
|
|
|
974 \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof.
|
|
|
975 \gdef\buildScore{\buildSingleScore}% Set next score to be single
|
|
|
976 \ignorespaces
|
|
|
977 }
|
|
|
978 \def\noLine{%
|
|
|
979 \gdef\buildScore{\buildNoScore}% Set next score to this type
|
|
|
980 \ignorespaces
|
|
|
981 }
|
|
|
982 \def\alwaysNoLine{%
|
|
|
983 \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof.
|
|
|
984 \gdef\buildScore{\buildNoScore}% Set next score to be blank
|
|
|
985 \ignorespaces
|
|
|
986 }
|
|
|
987 \def\solidLine{%
|
|
|
988 \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
|
|
|
989 \ignorespaces
|
|
|
990 }
|
|
|
991 \def\alwaysSolidLine{%
|
|
|
992 \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof
|
|
|
993 \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
|
|
|
994 \ignorespaces
|
|
|
995 }
|
|
|
996 \def\dottedLine{%
|
|
|
997 \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
|
|
|
998 \ignorespaces
|
|
|
999 }
|
|
|
1000 \def\alwaysDottedLine{%
|
|
|
1001 \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof
|
|
|
1002 \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
|
|
|
1003 \ignorespaces
|
|
|
1004 }
|
|
|
1005 \def\dashedLine{%
|
|
|
1006 \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
|
|
|
1007 \ignorespaces
|
|
|
1008 }
|
|
|
1009 \def\alwaysDashedLine{%
|
|
|
1010 \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof
|
|
|
1011 \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
|
|
|
1012 \ignorespaces
|
|
|
1013 }
|
|
|
1014 \def\kernHyps#1{%
|
|
|
1015 \gdef\hypKernAmt{#1}%
|
|
|
1016 \ignorespaces
|
|
|
1017 }
|
|
|
1018 \def\insertBetweenHyps#1{%
|
|
|
1019 \gdef\theHypSeparation{#1}%
|
|
|
1020 \ignorespaces
|
|
|
1021 }
|
|
|
1022
|
|
|
1023 \def\centerAlignProof{%
|
|
|
1024 \def\centerAlignFlag{Y}%
|
|
|
1025 \def\bottomAlignFlag{N}%
|
|
|
1026 \ignorespaces
|
|
|
1027 }
|
|
|
1028 \def\bottomAlignProof{%
|
|
|
1029 \def\centerAlignFlag{N}%
|
|
|
1030 \def\bottomAlignFlag{Y}%
|
|
|
1031 \ignorespaces
|
|
|
1032 }
|
|
|
1033 \def\normalAlignProof{%
|
|
|
1034 \def\centerAlignFlag{N}%
|
|
|
1035 \def\bottomAlignFlag{N}%
|
|
|
1036 \ignorespaces
|
|
|
1037 }
|
|
|
1038
|
|
|
1039 \def\LeftLabel#1{%
|
|
|
1040 \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}%
|
|
|
1041 \ignorespaces
|
|
|
1042 }
|
|
|
1043 \def\RightLabel#1{%
|
|
|
1044 \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}%
|
|
|
1045 \ignorespaces
|
|
|
1046 }
|
|
|
1047
|
|
|
1048 \def\buildScoreLabels{%
|
|
|
1049 \scoreHeight = \ht\myBoxD%
|
|
|
1050 \scoreDepth = \dp\myBoxD%
|
|
|
1051 \leftLowerAmt=\ht\myBoxLL%
|
|
|
1052 \advance \leftLowerAmt by -\dp\myBoxLL%
|
|
|
1053 \advance \leftLowerAmt by -\scoreHeight%
|
|
|
1054 \advance \leftLowerAmt by \scoreDepth%
|
|
|
1055 \leftLowerAmt=.5\leftLowerAmt%
|
|
|
1056 \rightLowerAmt=\ht\myBoxRL%
|
|
|
1057 \advance \rightLowerAmt by -\dp\myBoxRL%
|
|
|
1058 \advance \rightLowerAmt by -\scoreHeight%
|
|
|
1059 \advance \rightLowerAmt by \scoreDepth%
|
|
|
1060 \rightLowerAmt=.5\rightLowerAmt%
|
|
|
1061 \displace = \curScoreStart%
|
|
|
1062 \advance\displace by -\wd\myBoxLL%
|
|
|
1063 \global\setbox\myBoxD =%
|
|
|
1064 \hbox{\hskip\displace%
|
|
|
1065 \lower\leftLowerAmt\copy\myBoxLL%
|
|
|
1066 \box\myBoxD%
|
|
|
1067 \lower\rightLowerAmt\copy\myBoxRL}%
|
|
|
1068 \global\thisAboveSkip = \ht\myBoxLL%
|
|
|
1069 \global\advance \thisAboveSkip by -\leftLowerAmt%
|
|
|
1070 \global\advance \thisAboveSkip by -\scoreHeight%
|
|
|
1071 \ifnum \thisAboveSkip<0 %
|
|
|
1072 \global\thisAboveSkip=0pt%
|
|
|
1073 \fi%
|
|
|
1074 \displace = \ht\myBoxRL%
|
|
|
1075 \advance \displace by -\rightLowerAmt%
|
|
|
1076 \advance \displace by -\scoreHeight%
|
|
|
1077 \ifnum \displace<0 %
|
|
|
1078 \displace=0pt%
|
|
|
1079 \fi%
|
|
|
1080 \ifnum \displace>\thisAboveSkip %
|
|
|
1081 \global\thisAboveSkip=\displace%
|
|
|
1082 \fi%
|
|
|
1083 \global\thisBelowSkip = \dp\myBoxLL%
|
|
|
1084 \global\advance\thisBelowSkip by \leftLowerAmt%
|
|
|
1085 \global\advance\thisBelowSkip by -\scoreDepth%
|
|
|
1086 \ifnum\thisBelowSkip<0 %
|
|
|
1087 \global\thisBelowSkip = 0pt%
|
|
|
1088 \fi%
|
|
|
1089 \displace = \dp\myBoxRL%
|
|
|
1090 \advance\displace by \rightLowerAmt%
|
|
|
1091 \advance\displace by -\scoreDepth%
|
|
|
1092 \ifnum\displace<0 %
|
|
|
1093 \displace = 0pt%
|
|
|
1094 \fi%
|
|
|
1095 \ifnum\displace>\thisBelowSkip%
|
|
|
1096 \global\thisBelowSkip = \displace%
|
|
|
1097 \fi%
|
|
|
1098 \global\thisAboveSkip = -\thisAboveSkip%
|
|
|
1099 \global\thisBelowSkip = -\thisBelowSkip%
|
|
|
1100 \global\advance\thisAboveSkip by\extraVskip% Extra space above line
|
|
|
1101 \global\advance\thisBelowSkip by\extraVskip% Extra space below line
|
|
|
1102 }
|
|
|
1103
|
|
|
1104 \def\resetInferenceDefaults{%
|
|
|
1105 \global\def\theHypSeparation{\defaultHypSeparation}%
|
|
|
1106 \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
|
|
|
1107 \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
|
|
|
1108 \global\def\buildScore{\alwaysBuildScore}%
|
|
|
1109 \global\def\theScoreFiller{\alwaysScoreFiller}%
|
|
|
1110 \gdef\hypKernAmt{0pt}% Restore to zero kerning.
|
|
|
1111 }
|
|
|
1112
|
|
|
1113
|
|
|
1114 \def\rootAtBottom{%
|
|
|
1115 \global\def\rootAtBottomFlag{Y}%
|
|
|
1116 }
|
|
|
1117
|
|
|
1118 \def\rootAtTop{%
|
|
|
1119 \global\def\rootAtBottomFlag{N}%
|
|
|
1120 }
|
|
|
1121
|
|
|
1122 \def\resetRootPosition{%
|
|
|
1123 \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag}
|
|
|
1124 }
|
|
|
1125
|
|
|
1126 \def\alwaysRootAtBottom{%
|
|
|
1127 \global\def\defaultRootAtBottomFlag{Y}
|
|
|
1128 \rootAtBottom
|
|
|
1129 }
|
|
|
1130
|
|
|
1131 \def\alwaysRootAtTop{%
|
|
|
1132 \global\def\defaultRootAtBottomFlag{N}
|
|
|
1133 \rootAtTop
|
|
|
1134 }
|
|
|
1135
|
|
|
1136
|
