Papers/2015/atton-thesis: paper/bussproofs.sty annotate

annotate paper/bussproofs.sty @ 78:6f699b37dc55

Add original number count

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Wed, 18 Feb 2015 12:26:17 +0900
parents	1181b4facaf9
children

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

Mercurial > hg > Papers > 2015 > atton-thesis

annotate paper/bussproofs.sty @ 78:6f699b37dc55