--- a/final_main/chapter2.tex	Tue Feb 19 14:14:30 2019 +0900
+++ b/final_main/chapter2.tex	Tue Feb 19 14:30:13 2019 +0900
@@ -104,10 +104,9 @@
 
 \section{木構造の再構成}
 バイナリツリーでの接続のため、 Node が切断されたことを検知できないと構成した木構造が崩れてしまい、新しい Node を適切な場所に接続できなくなってしまう。そこで木構造を崩さずに再構成を行う必要がある。
-	TreeVNC の木構造のネットワークトポロジーは Root Node が持っている nodeList で管理している。
-	→ Node の接続が切れたら Root Node に知らせる必要がある。
-	→ LOST_CHILD というメッセージで Node の切断を検知・木の再構成を行う
-	→ LOST_CHILD の検出方法には MulticastQueue を使用している(一定期間 MulticastQueue から画像データが取得されない場合、 MemoryOverFlow を回避するために Timeout スレッドが用意されており、これを検知した場合 Node の接続が切れたと判断する)。
+
+TreeVNC の木構造のネットワークトポロジーは Root Node が持っている nodeList で管理している。
+Node の接続が切れた場合、Root Node に切断を知らせる必要がある。この時 LOST\_CHILD というメッセージで Node の切断を検知・木の再構成を行う。LOST\_CHILD の検出方法には MulticastQueue を使用している(一定期間 MulticastQueue から画像データが取得されない場合、 MemoryOverFlow を回避するために Timeout スレッドが用意されており、これを検知した場合 Node の接続が切れたと判断する)。
 
 \section{ZRLEE}
 

Binary file final_main/main.pdf has changed

--- a/final_pre/Makefile	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-# Created by Daichi Toma on Nov 16, 2011
-
-TARGET=finalPre
-
-LATEX=platex
-BIBTEX=pbibtex
-DVIPDF=dvipdfmx -p a4
-#You need setting "-l" option if You think You get a landscape PDF
-#DVIPDF_OPT=-l
-
-#Embed fonts
-#DVIPDF_OPT=-f hiraginoEmbed.map
-
-.SUFFIXES: .tex .dvi .pdf
-
-.tex.dvi:
-	$(LATEX) $<
-	$(BIBTEX) $(TARGET)
-	$(LATEX) $<
-	$(LATEX) $<
-
-.dvi.pdf:
-	$(DVIPDF) $(DVIPDF_OPT) $<
-
-
-all: $(TARGET).pdf
-	open $(TARGET).pdf
-
-dvi: $(TARGET).dvi
-
-pdf: $(TARGET).pdf
-
-
-clean:
-	rm -f *.dvi *.aux *.log *.ps *.gz *.bbl *.blg *.toc *~ *.core
-

--- a/final_pre/auto/midterm.el	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(TeX-add-style-hook
- "midterm"
- (lambda ()
-   (TeX-add-to-alist 'LaTeX-provided-class-options
-                     '(("jarticle" "twocolumn" "twoside" "9.5pt")))
-   (TeX-add-to-alist 'LaTeX-provided-package-options
-                     '(("graphicx" "dvipdfmx")))
-   (add-to-list 'LaTeX-verbatim-environments-local "lstlisting")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "path")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "lstinline")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "path")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "lstinline")
-   (TeX-run-style-hooks
-    "latex2e"
-    "dummy"
-    "jarticle"
-    "jart10"
-    "graphicx"
-    "picins"
-    "fancyhdr"
-    "abstract"
-    "url"
-    "bussproofs"
-    "listings"
-    "jlisting")
-   (LaTeX-add-bibliographies
-    "reference"))
- :latex)
-

--- a/final_pre/bussproofs.sty	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1136 +0,0 @@
-%
-\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
-% bussproofs.sty.  Version 1.1
-%     (c) 1994,1995,1996,2004,2005,2006, 2011. 
-%     Copyright retained by Samuel R. Buss.
-%
-% ==== Legal statement: ====
-% This work may be distributed and/or modified under the
-% conditions of the LaTeX Project Public License, either version 1.3
-% of this license or (at your option) any later version.
-% The latest version of this license is in
-%  http://www.latex-project.org/lppl.txt.
-% and version 1.3 or later is part of all distributions of LaTeX
-% version 2005/12/1 or later.
-%
-% This work has the LPPL maintenance status 'maintained'.
-%
-% The Current Maintainer of the work is Sam Buss.
-%
-% This work consists of bussproofs.sty.
-%  =====
-% Informal summary of legal situation:
-%     This software may be used and distributed freely, except that
-%     if you make changes, you must change the file name to be different
-%     than bussproofs.sty to avoid compatibility problems.
-% The terms of the LaTeX Public License are the legally controlling terms
-%     and override any contradictory terms of the "informal situation".
-%
-%     Please report comments and bugs to sbuss@ucsd.edu.
-%
-%  Thanks to Felix Joachimski for making changes to let these macros
-%   work in plain TeX in addition to LaTeX.  Nothing has been done
-%   to see if they work in AMSTeX.  The comments below mostly
-%   are written for LaTeX, however.
-%  July 2004, version 0.7
-%       - bug fix, right labels with descenders inserted too much space.
-%         Thanks to Peter Smith for finding this bug,
-%     see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
-%  March 2005, version 0.8.
-%   Added a default definition for \fCenter at Denis Kosygin's
-%   suggestion.
-%  September 2005, version 0.9.
-%       Fixed some subtle spacing problems, by adding %'s to the end of
-%   few lines where they were inadvertantly omitted.  Thanks to
-%   Arnold Beckmann for finding and fixing this problem.
-%  April 2006, version 0.9.1.  Updated comments and testbp2.tex file.
-%       No change to the actual macros.
-%  June 2006, version 1.0.  The first integer numbered release.
-%       New feature: root of proof may now be at the bottom instead of
-%       at just the top.  Thanks to Alex Hertel for the suggestion to implement
-%       this.
-%  June 2011, version 1.1.  
-%       New feature: 4-ary and 5-ary inferences.  Thanks to Thomas Strathmann
-%       for taking the initiative to implement these.
-%         Four new commands: QuaternaryInf(C) and QuinaryInf(C).
-%       Bug fix: \insertBetweenHyps now works for proofs with root at top and
-%            three or more hypotheses..
-
-% A good exposition of how to use bussproofs.sty (version 0.9) has been written
-%  by Peter Smith and is available on the internet.
-% The comments below also describe the features of bussproofs.sty,
-%  including user-modifiable parameters.
-
-%  bussproofs.sty allows the construction of proof trees in the
-%     style of the sequent calculus and many other proof systems
-%     One novel feature of these macros is they support the horizontal
-%     alignment according to some center point specified with the
-%     command \fCenter.  This is the style often used in sequent
-%     calculus proofs.
-%     Proofs are specified in left-to-right traversal order.
-%       For example a proof
-%               A   B
-%                               -----
-%                          D      C
-%                         ---------
-%                             E
-%
-%     if given in the order D,A,B,C,E.  Each line in the proof is
-%     specified according to the arity of the inference which generates
-%     it.  Thus, E would be specified with a \BinaryInf  or  \BinaryInfC
-%     command.
-%
-%     The above proof tree could be displayed with the commands:
-%
-%               \AxiomC{D}
-%               \AxiomC{A}
-%               \AxiomC{B}
-%               \BinaryInfC{C}
-%               \BinaryInfC{E}
-%               \DisplayProof
-%
-%     Inferences in a proof may be nullary (axioms), unary, binary, or
-%     trinary.
-%
-%     IMPORTANT:  You must give the \DisplayProof command to make the proof
-%      be printed.  To display a centered proof on a line by itself,
-%      put the proof inside \begin{center} ... \end{center}.
-%
-%     There are two styles for specifying horizontal centering of
-%     lines (formulas or sequents) in a proof.  One format \AxiomC{...}
-%     just centers the formula {...} in the usual way.  The other
-%     format is \Axiom$...\fCenter...$.  Here,  the \fCenter specifies
-%     the center of the formula.  (It is permissable for \fCenter to
-%     generate typeset material; in fact, I usually define it to generate
-%     the sequent arrow.)  In unary inferences, the \fCenter
-%     positions will be vertically aligned in the upper and lower lines of
-%     the inference.  Unary, Binary, Trinary inferences are specified
-%     with the same format as Axioms.  The two styles of centering
-%     lines may be combined in a single proof.
-%
-%     By using the optional \EnableBpAbbreviations command, various
-%   abbreviated two or three letter commands are enabled.  This allows,
-%   in particular:
-%   \AX and \AXC for \Axiom and \AxiomC, (resp.),
-%   \DP for \DisplayProof,
-%   \BI and \BIC for \BinaryInf and \BinaryInfC,
-%   \UI and \UIC for \UnaryInf  and \UnaryInfC,
-%   \TI and \TIC for \TrinaryInf and \TrinaryInfC,
-%   \LL and \RL for \LeftLabel and \RightLabel.
-%   See the source code below for additional abbreviations.
-%     The enabling of these short abbreviations is OPTIONAL, since
-%       there is the possibility of conflicting with names from other
-%       macro packages.
-%
-%     By default, the inferences have single horizontal lines (scores)
-%       This can be overridden using the \doubleLine, \noLine commands.
-%       These two commands affect only the next inference.  You can make
-%   make a permanent override that applies to the rest of the current
-%       proof using \alwaysDoubleLine and \alwaysNoLine.  \singleLine
-%   and \alwaysSingleLine work in the analogous way.
-%
-%     The macros do their best to give good placements of for the
-%     parts of the proof.  Several macros allow you to override the
-%     defaults.  These are \insertBetweenHyps{...} which overrides
-%     the default spacing between hypotheses of Binary and Trinary
-%     inferences with {...}.  And \kernHyps{...} specifies a distance
-%     to shift the whole block of hypotheses to the right (modifying
-%     the default center position.
-%       Other macros set the vertical placement of the whole proof.
-%     The default is to try to do a good job of placement for inferences
-%     included in text.  Two other useful macros are: \bottomAlignProof
-%     which aligns the hbox output by \DisplayProof according to the base
-%     of the bottom line of the proof, and \centerAlignProof which
-%     does a precise center vertical alignment.
-%
-%     Often, one wishes to place a label next to an inference, usually
-%   to specify the type of inference.  These labels can be placed
-%       by using the commands \LeftLabel{...} and \RightLabel{...}
-%       immediately before the command which specifies the inference.
-%       For example, to generate
-%
-%                       A     B
-%                      --------- X
-%                          C
-%
-%       use the commands
-%             \AxiomC{A}
-%             \AxiomC{B}
-%             \RightLabel{X}
-%             \BinaryInfC{C}
-%             \DisplayProof
-%
-%     The \DisplayProof command just displays the proof as a text
-%   item.  This allows you to put proofs anywhere normal text
-%   might appear; for example, in a paragraph, in a table, in
-%   a tabbing environment, etc.  When displaying a proof as inline text,
-%   you should write \DisplayProof{}  (with curly brackets) so that
-%   LaTeX will not "eat" the white space following the \DisplayProof
-%   command.
-%     For displaying proofs in a centered display:  Do not use the \[...\]
-%   construction (nor $$...$$).  Instead use
-%   \begin{center} ... \DisplayProof\end{center}.
-%     Actually there is a better construction to use instead of the
-%   \begin{center}...\DisplayProof\end{center}.  This is to
-%   write
-%       \begin{prooftree} ... \end{prooftree}.
-%       Note there is no \DisplayProof used for this: the
-%   \end{prooftree} automatically supplies the \DisplayProof
-%   command.
-%
-%     Warning: Any commands that set line types or set vertical or
-%   horizontal alignment that are given AFTER the \DisplayProof
-%   command will affect the next proof, no matter how distant.
-
-
-
-
-% Usages:
-% =======
-%
-%   \Axiom$<antecedent>\fCenter<succedent>$
-%
-%   \AxiomC{<whole sequent or formula}
-%
-%   Note that the use of surrounding {}'s is mandatory in \AxiomC and
-%   is prohibited in $\Axiom.  On the other hand, the $'s are optional
-%   in \AxiomC and are mandatory in \Axiom.  To typeset the argument
-%   to \AxiomC in math mode, you must use $'s (or \(...\) ).
-%   The same comments apply to the inference commands below.
-%
-%   \UnaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \UnaryInfC{<whole sequent or formula>}
-%
-%   \BinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \BinaryInfC{<whole sequent or formula>}
-%
-%   \TrinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \TrinaryInfC{<whole sequent or formula>}
-%
-%   \QuaternaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \QuaternaryInfC{<whole sequent or formula>}
-%
-%   \QuinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \QuinaryInfC{<whole sequent or formula>}
-%
-%   \LeftLabel{<text>} - Puts <text> as a label to the left
-%             of the next inference line.  (Works even if
-%             \noLine is used too.)
-%
-%   \RightLabel{<text>} - Puts <text> as a label to the right of the
-%             next inference line.  (Also works with \noLine.)
-%
-%   \DisplayProof - outputs the whole proof tree (and finishes it).
-%           The proof tree is output as an hbox.
-%
-%
-%   \kernHyps{<dimen>}  - Slides the upper hypotheses right distance <dimen>
-%             (This is similar to shifting conclusion left)
-%           - kernHyps works with Unary, Binary and Trinary
-%             inferences and with centered or uncentered sequents.
-%           - Negative values for <dimen> are permitted.
-%
-%   \insertBetweenHyps{...} - {...} will be inserted between the upper
-%             hypotheses of a Binary or Trinary Inferences.
-%                         It is possible to use negative horizontal space
-%                 to push them closer together (and even overlap).
-%             This command affects only the next inference.
-%
-%   \doubleLine         - Makes the current (ie, next) horizontal line doubled
-%
-%   \alwaysDoubleLine   - Makes lines doubled for rest of proof
-%
-%   \singleLine     - Makes the current (ie, next) line single
-%
-%   \alwaysSingleLine   - Undoes \alwaysDoubleLine or \alwaysNoLine.
-%
-%   \noLine     - Make no line at all at current (ie next) inference.
-%
-%   \alwaysNoLine       - Makes no lines for rest of proof. (Untested)
-%
-%   \solidLine      - Does solid horizontal line for current inference
-%
-%   \dottedLine     - Does dotted horizontal line for current inference
-%
-%   \dashedLine     - Does dashed horizontal line for current inference
-%
-%   \alwaysSolidLine    - Makes the indicated change in line type, permanently
-%   \alwaysDashedLine       until end of proof or until overridden.
-%   \alwaysDottedLine
-%
-%   \bottomAlignProof   - Vertically align proof according to its bottom line.
-%   \centerAlignProof   - Vertically align proof proof precisely in its center.
-%   \normalAlignProof   - Overrides earlier bottom/center AlignProof commands.
-%             The default alignment will look good in most cases,
-%               whether the proof is displayed or is
-%               in-line.  Other alignments may be more
-%               appropriate when putting proofs in tables or
-%               pictures, etc.  For custom alignments, use
-%               TeX's raise commands.
-%
-%   \rootAtTop  - specifies that proofs have their root a the top.  That it,
-%                 proofs will be "upside down".
-%   \rootAtBottom - (default) Specifies that proofs have root at the bottom
-%         The \rootAtTop and \rootAtBottom commands apply *only* to the
-%         current proof.  If you want to make them persistent, use one of
-%         the next two commands:
-%   \alwaysRootAtTop
-%   \alwaysRootAtBottom (default)
-%
-
-% Optional short abbreviations for commands:
-\def\EnableBpAbbreviations{%
-    \let\AX\Axiom
-    \let\AXC\AxiomC
-    \let\UI\UnaryInf
-    \let\UIC\UnaryInfC
-    \let\BI\BinaryInf
-    \let\BIC\BinaryInfC
-    \let\TI\TrinaryInf
-    \let\TIC\TrinaryInfC
-    \let\QI\QuaternaryInf
-    \let\QIC\QuaternaryInfC
-    \let\QuI\QuinaryInf
-    \let\QuIC\QuinaryInfC
-    \let\LL\LeftLabel
-    \let\RL\RightLabel
-    \let\DP\DisplayProof
-}
-
-% Parameters which control the style of the proof trees.
-% The user may wish to override these parameters locally or globally.
-%   BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
-%   future incompatibilities).  Instead, you should change them in your
-%   TeX document right after including this style file in the
-%   header material of your LaTeX document.
-
-\def\ScoreOverhang{4pt}         % How much underlines extend out
-\def\ScoreOverhangLeft{\ScoreOverhang}
-\def\ScoreOverhangRight{\ScoreOverhang}
-
-\def\extraVskip{2pt}            % Extra space above and below lines
-\def\ruleScoreFiller{\hrule}        % Horizontal rule filler.
-\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}}
-\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}
-\def\defaultScoreFiller{\ruleScoreFiller}  % Default horizontal filler.
-\def\defaultBuildScore{\buildSingleScore}  % In \singleLine mode at start.
-
-\def\defaultHypSeparation{\hskip.2in}   % Used if \insertBetweenHyps isn't given
-
-\def\labelSpacing{3pt}      % Horizontal space separating labels and lines
-
-\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex}
-            % Space above and below a prooftree display.
-
-\def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom
-%\def\defaultRootPosition{\buildRootTop}  % Makes all proofs upside down
-
-\ifx\fCenter\undefined
-\def\fCenter{\relax}
-\fi
-
-%
-% End of user-modifiable parameters.
-% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% Here are some internal paramenters and defaults.  Not really intended
-%  to be user-modifiable.
-
-\def\theHypSeparation{\defaultHypSeparation}
-\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler.
-\def\alwaysBuildScore{\defaultBuildScore}
-\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler.
-\def\buildScore{\alwaysBuildScore}   %This command builds the score.
-\def\hypKernAmt{0pt}    % Initial setting for kerning the hypotheses.
-
-\def\defaultLeftLabel{}
-\def\defaultRightLabel{}
-
-\def\myTrue{Y}
-\def\bottomAlignFlag{N}
-\def\centerAlignFlag{N}
-\def\defaultRootAtBottomFlag{Y}
-\def\rootAtBottomFlag{Y}
-
-% End of internal parameters and defaults.
-
-\expandafter\ifx\csname newenvironment\endcsname\relax%
-% If in TeX:
-\message{\BPmessage}
-\def\makeatletter{\catcode`\@=11\relax}
-\def\makeatother{\catcode`\@=12\relax}
-\makeatletter
-\def\newcount{\alloc@0\count\countdef\insc@unt}
-\def\newdimen{\alloc@1\dimen\dimendef\insc@unt}
-\def\newskip{\alloc@2\skip\skipdef\insc@unt}
-\def\newbox{\alloc@4\box\chardef\insc@unt}
-\makeatother
-\else
-% If in LaTeX
-\typeout{\BPmessage}
-\newenvironment{prooftree}%
-{\begin{center}\proofSkipAmount \leavevmode}%
-{\DisplayProof \proofSkipAmount \end{center} }
-\fi
-
-\def\thecur#1{\csname#1\number\theLevel\endcsname}
-
-\newcount\theLevel    % This counter is the height of the stack.
-\global\theLevel=0      % Initialized to zero
-\newcount\myMaxLevel
-\global\myMaxLevel=0
-\newbox\myBoxA      % Temporary storage boxes
-\newbox\myBoxB
-\newbox\myBoxC
-\newbox\myBoxD
-\newbox\myBoxLL     % Boxes for the left label and the right label.
-\newbox\myBoxRL
-\newdimen\thisAboveSkip     %Internal use: amount to skip above line
-\newdimen\thisBelowSkip     %Internal use: amount to skip below line
-\newdimen\newScoreStart     % More temporary storage.
-\newdimen\newScoreEnd
-\newdimen\newCenter
-\newdimen\displace
-\newdimen\leftLowerAmt%     Amount to lower left label
-\newdimen\rightLowerAmt%    Amount to lower right label
-\newdimen\scoreHeight%      Score height
-\newdimen\scoreDepth%       Score Depth
-\newdimen\htLbox%
-\newdimen\htRbox%
-\newdimen\htRRbox%
-\newdimen\htRRRbox%
-\newdimen\htAbox%
-\newdimen\htCbox%
-
-\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
-\setbox\myBoxRL=\hbox{\defaultRightLabel}%
-
-\def\allocatemore{%
-    \ifnum\theLevel>\myMaxLevel%
-        \expandafter\newbox\curBox%
-        \expandafter\newdimen\curScoreStart%
-        \expandafter\newdimen\curCenter%
-        \expandafter\newdimen\curScoreEnd%
-        \global\advance\myMaxLevel by1%
-    \fi%
-}
-
-\def\prepAxiom{%
-    \advance\theLevel by1%
-    \edef\curBox{\thecur{myBox}}%
-    \edef\curScoreStart{\thecur{myScoreStart}}%
-    \edef\curCenter{\thecur{myCenter}}%
-    \edef\curScoreEnd{\thecur{myScoreEnd}}%
-    \allocatemore%
-}
-
-\def\Axiom$#1\fCenter#2${%
-    % Get level and correct names set.
-    \prepAxiom%
-    % Define the boxes
-    \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
-    \setbox\myBoxB=\hbox{$#2$}%
-    \global\setbox\curBox=%
-         \hbox{\hskip\ScoreOverhangLeft\relax%
-        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
-    % Set the relevant dimensions for the boxes
-    \global\curScoreStart=0pt \relax
-    \global\curScoreEnd=\wd\curBox \relax
-    \global\curCenter=\wd\myBoxA \relax
-    \global\advance \curCenter by \ScoreOverhangLeft%
-    \ignorespaces
-}
-
-\def\AxiomC#1{      % Note argument not in math mode
-    % Get level and correct names set.
-    \prepAxiom%
-        % Define the box.
-    \setbox\myBoxA=\hbox{#1}%
-    \global\setbox\curBox =%
-        \hbox{\hskip\ScoreOverhangLeft\relax%
-                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
-    % Set the relevant dimensions for the boxes
-        \global\curScoreStart=0pt \relax
-        \global\curScoreEnd=\wd\curBox \relax
-        \global\curCenter=.5\wd\curBox \relax
-        \global\advance \curCenter by \ScoreOverhangLeft%
-    \ignorespaces
-}
-
-\def\prepUnary{%
-    \ifnum \theLevel<1
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\curBox{\thecur{myBox}}%
-    \edef\curScoreStart{\thecur{myScoreStart}}%
-    \edef\curCenter{\thecur{myCenter}}%
-    \edef\curScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\UnaryInf$#1\fCenter#2${%
-    \prepUnary%
-    \buildConclusion{#1}{#2}%
-    \joinUnary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\UnaryInfC#1{
-    \prepUnary%
-    \buildConclusionC{#1}%
-    %Align and join the curBox and the new box into one vbox.
-    \joinUnary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\prepBinary{%
-    \ifnum\theLevel<2
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\BinaryInf$#1\fCenter#2${%
-    \prepBinary%
-    \buildConclusion{#1}{#2}%
-    \joinBinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\BinaryInfC#1{%
-    \prepBinary%
-    \buildConclusionC{#1}%
-    \joinBinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\prepTrinary{%
-    \ifnum\theLevel<3
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\TrinaryInf$#1\fCenter#2${%
-    \prepTrinary%
-    \buildConclusion{#1}{#2}%
-    \joinTrinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\TrinaryInfC#1{%
-    \prepTrinary%
-    \buildConclusionC{#1}%
-    \joinTrinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\def\prepQuaternary{%
-    \ifnum\theLevel<4
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rrcurBox{\thecur{myBox}}%   Set up names of very right hypothesis
-    \edef\rrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrcurCenter{\thecur{myCenter}}%
-    \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\QuaternaryInf$#1\fCenter#2${%
-    \prepQuaternary%
-    \buildConclusion{#1}{#2}%
-    \joinQuaternary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\QuaternaryInfC#1{%
-    \prepQuaternary%
-    \buildConclusionC{#1}%
-    \joinQuaternary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\joinQuaternary{% Construct the quarterary inference into a vbox.
-    % Join the four hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rrcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\rcurBox%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by3\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox
-                      \unhcopy\myBoxA\box\rrcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \htRRbox = \ht\rrcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\def\prepQuinary{%
-    \ifnum\theLevel<5
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rrrcurBox{\thecur{myBox}}%   Set up names of very very right hypothesis
-    \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrrcurCenter{\thecur{myCenter}}%
-    \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rrcurBox{\thecur{myBox}}%   Set up names of very right hypothesis
-    \edef\rrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrcurCenter{\thecur{myCenter}}%
-    \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\QuinaryInf$#1\fCenter#2${%
-    \prepQuinary%
-    \buildConclusion{#1}{#2}%
-    \joinQuinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\QuinaryInfC#1{%
-    \prepQuinary%
-    \buildConclusionC{#1}%
-    \joinQuinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\joinQuinary{% Construct the quinary inference into a vbox.
-    % Join the five hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rrrcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\rrcurBox%
-    \advance\lcurScoreEnd by\wd\rcurBox%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by4\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox
-                      \unhcopy\myBoxA\box\rrcurBox
-                      \unhcopy\myBoxA\box\rrrcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \htRRbox = \ht\rrcurBox%
-        \htRRRbox = \ht\rrrcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
-    % Define the boxes
-        \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
-        \setbox\myBoxB=\hbox{$#2$}%
-    % Put them together in \myBoxC
-    \setbox\myBoxC =%
-          \hbox{\hskip\ScoreOverhangLeft\relax%
-        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
-    % Calculate the center of the \myBoxC string.
-    \newScoreStart=0pt \relax%
-    \newCenter=\wd\myBoxA \relax%
-    \advance \newCenter by \ScoreOverhangLeft%
-    \newScoreEnd=\wd\myBoxC%
-}
-
-\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
-        % Define the box.
-    \setbox\myBoxA=\hbox{#1}%
-    \setbox\myBoxC =%
-        \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
-                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
-    % Calculate kerning to line up centers
-    \newScoreStart=0pt \relax%
-    \newCenter=.5\wd\myBoxC \relax%
-    \newScoreEnd=\wd\myBoxC%
-        \advance \newCenter by \ScoreOverhangLeft%
-}
-
-\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox
-    \global\advance\curCenter by -\hypKernAmt%
-    \ifnum\curCenter<\newCenter%
-        \displace=\newCenter%
-        \advance \displace by -\curCenter%
-        \kernUpperBox%
-    \else%
-        \displace=\curCenter%
-        \advance \displace by -\newCenter%
-        \kernLowerBox%
-    \fi%
-        \ifnum \newScoreStart < \curScoreStart %
-        \global \curScoreStart = \newScoreStart \fi%
-    \ifnum \curScoreEnd < \newScoreEnd %
-        \global \curScoreEnd = \newScoreEnd \fi%
-    % Leave room for the left label.
-    \ifnum \curScoreStart<\wd\myBoxLL%
-        \global\displace = \wd\myBoxLL%
-        \global\advance\displace by -\curScoreStart%
-        \kernUpperBox%
-        \kernLowerBox%
-    \fi%
-    % Draw the score
-    \buildScore%
-    % Form the score and labels into a box.
-    \buildScoreLabels%
-    % Form the new box and its dimensions
-    \ifx\rootAtBottomFlag\myTrue%
-        \buildRootBottom%
-    \else%
-        \buildRootTop%
-    \fi%
-    \global \curScoreStart=\newScoreStart%
-    \global \curScoreEnd=\newScoreEnd%
-    \global \curCenter=\newCenter%
-}
-
-\def\buildRootBottom{%
-    \global \setbox \curBox =%
-        \vbox{\box\curBox%
-            \vskip\thisAboveSkip \relax%
-            \nointerlineskip\box\myBoxD%
-            \vskip\thisBelowSkip \relax%
-            \nointerlineskip\box\myBoxC}%
-}
-
-\def\buildRootTop{%
-    \global \setbox \curBox =%
-        \vbox{\box\myBoxC%
-            \vskip\thisAboveSkip \relax%
-            \nointerlineskip\box\myBoxD%
-            \vskip\thisBelowSkip \relax%
-            \nointerlineskip\box\curBox}%
-}
-
-\def\kernUpperBox{%
-        \global\setbox\curBox =%
-            \hbox{\hskip\displace\box\curBox}%
-        \global\advance \curScoreStart by \displace%
-        \global\advance \curScoreEnd by \displace%
-        \global\advance\curCenter by \displace%
-}
-
-\def\kernLowerBox{%
-        \global\setbox\myBoxC =%
-            \hbox{\hskip\displace\unhbox\myBoxC}%
-        \global\advance \newScoreStart by \displace%
-        \global\advance \newScoreEnd by \displace%
-        \global\advance\newCenter by \displace%
-}
-
-\def\joinBinary{% Construct the binary inference into a vbox.
-    % Join the two hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htRbox = \ht\rcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-\def\joinTrinary{% Construct the trinary inference into a vbox.
-    % Join the three hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by2\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-\def\DisplayProof{%
-    % Display (and purge) the proof tree.
-    % Choose the appropriate vertical alignment.
-    \ifnum \theLevel=1 \relax \else%x
-        \errmessage{Proof tree badly specified.}%
-    \fi%
-    \edef\curBox{\thecur{myBox}}%
-    \ifx\bottomAlignFlag\myTrue%
-        \displace=0pt%
-    \else%
-        \displace=.5\ht\curBox%
-        \ifx\centerAlignFlag\myTrue\relax
-        \else%
-                \advance\displace by -3pt%
-        \fi%
-    \fi%
-    \leavevmode%
-    \lower\displace\hbox{\copy\curBox}%
-    \global\theLevel=0%
-    \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always"
-    \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always"
-    \global\def\bottomAlignFlag{N}%
-    \global\def\centerAlignFlag{N}%
-    \resetRootPosition
-    \resetInferenceDefaults%
-    \ignorespaces
-}
-
-\def\buildSingleScore{% Make an hbox with a single score.
-    \displace=\curScoreEnd%
-    \advance \displace by -\curScoreStart%
-    \global\setbox \myBoxD =%
-        \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}%
-    %\global\setbox \myBoxD =%
-        %\hbox{\hskip\curScoreStart\relax \box\myBoxD}%
-}
-
-\def\buildDoubleScore{% Make an hbox with a double score.
-    \buildSingleScore%
-    \global\setbox\myBoxD=%
-        \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}%
-}
-
-\def\buildNoScore{% Make an hbox with no score (raise a little anyway)
-    \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}%
-}
-
-\def\doubleLine{%
-    \gdef\buildScore{\buildDoubleScore}% Set next score to this type
-    \ignorespaces
-}
-\def\alwaysDoubleLine{%
-    \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof.
-    \gdef\buildScore{\buildDoubleScore}% Set next score to be double
-    \ignorespaces
-}
-\def\singleLine{%
-    \gdef\buildScore{\buildSingleScore}% Set next score to be single
-    \ignorespaces
-}
-\def\alwaysSingleLine{%
-    \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof.
-    \gdef\buildScore{\buildSingleScore}% Set next score to be single
-    \ignorespaces
-}
-\def\noLine{%
-    \gdef\buildScore{\buildNoScore}% Set next score to this type
-    \ignorespaces
-}
-\def\alwaysNoLine{%
-    \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof.
-    \gdef\buildScore{\buildNoScore}% Set next score to be blank
-    \ignorespaces
-}
-\def\solidLine{%
-    \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
-    \ignorespaces
-}
-\def\alwaysSolidLine{%
-    \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof
-    \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
-    \ignorespaces
-}
-\def\dottedLine{%
-    \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
-    \ignorespaces
-}
-\def\alwaysDottedLine{%
-    \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof
-    \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
-    \ignorespaces
-}
-\def\dashedLine{%
-    \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
-    \ignorespaces
-}
-\def\alwaysDashedLine{%
-    \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof
-    \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
-    \ignorespaces
-}
-\def\kernHyps#1{%
-    \gdef\hypKernAmt{#1}%
-    \ignorespaces
-}
-\def\insertBetweenHyps#1{%
-    \gdef\theHypSeparation{#1}%
-    \ignorespaces
-}
-
-\def\centerAlignProof{%
-    \def\centerAlignFlag{Y}%
-    \def\bottomAlignFlag{N}%
-    \ignorespaces
-}
-\def\bottomAlignProof{%
-    \def\centerAlignFlag{N}%
-    \def\bottomAlignFlag{Y}%
-    \ignorespaces
-}
-\def\normalAlignProof{%
-    \def\centerAlignFlag{N}%
-    \def\bottomAlignFlag{N}%
-    \ignorespaces
-}
-
-\def\LeftLabel#1{%
-    \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}%
-    \ignorespaces
-}
-\def\RightLabel#1{%
-    \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}%
-    \ignorespaces
-}
-
-\def\buildScoreLabels{%
-    \scoreHeight = \ht\myBoxD%
-    \scoreDepth = \dp\myBoxD%
-    \leftLowerAmt=\ht\myBoxLL%
-    \advance \leftLowerAmt by -\dp\myBoxLL%
-    \advance \leftLowerAmt by -\scoreHeight%
-    \advance \leftLowerAmt by \scoreDepth%
-    \leftLowerAmt=.5\leftLowerAmt%
-    \rightLowerAmt=\ht\myBoxRL%
-    \advance \rightLowerAmt by -\dp\myBoxRL%
-    \advance \rightLowerAmt by -\scoreHeight%
-    \advance \rightLowerAmt by \scoreDepth%
-    \rightLowerAmt=.5\rightLowerAmt%
-    \displace = \curScoreStart%
-    \advance\displace by -\wd\myBoxLL%
-    \global\setbox\myBoxD =%
-        \hbox{\hskip\displace%
-            \lower\leftLowerAmt\copy\myBoxLL%
-            \box\myBoxD%
-            \lower\rightLowerAmt\copy\myBoxRL}%
-    \global\thisAboveSkip = \ht\myBoxLL%
-    \global\advance \thisAboveSkip by -\leftLowerAmt%
-    \global\advance \thisAboveSkip by -\scoreHeight%
-    \ifnum \thisAboveSkip<0 %
-        \global\thisAboveSkip=0pt%
-    \fi%
-    \displace = \ht\myBoxRL%
-    \advance \displace by -\rightLowerAmt%
-    \advance \displace by -\scoreHeight%
-    \ifnum \displace<0 %
-        \displace=0pt%
-    \fi%
-    \ifnum \displace>\thisAboveSkip %
-        \global\thisAboveSkip=\displace%
-    \fi%
-    \global\thisBelowSkip = \dp\myBoxLL%
-    \global\advance\thisBelowSkip by \leftLowerAmt%
-    \global\advance\thisBelowSkip by -\scoreDepth%
-    \ifnum\thisBelowSkip<0 %
-        \global\thisBelowSkip = 0pt%
-    \fi%
-    \displace = \dp\myBoxRL%
-    \advance\displace by \rightLowerAmt%
-    \advance\displace by -\scoreDepth%
-    \ifnum\displace<0 %
-        \displace = 0pt%
-    \fi%
-    \ifnum\displace>\thisBelowSkip%
-        \global\thisBelowSkip = \displace%
-    \fi%
-    \global\thisAboveSkip = -\thisAboveSkip%
-    \global\thisBelowSkip = -\thisBelowSkip%
-    \global\advance\thisAboveSkip by\extraVskip% Extra space above line
-    \global\advance\thisBelowSkip by\extraVskip% Extra space below line
-}
-
-\def\resetInferenceDefaults{%
-    \global\def\theHypSeparation{\defaultHypSeparation}%
-    \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
-    \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
-    \global\def\buildScore{\alwaysBuildScore}%
-    \global\def\theScoreFiller{\alwaysScoreFiller}%
-    \gdef\hypKernAmt{0pt}% Restore to zero kerning.
-}
-
-
-\def\rootAtBottom{%
-    \global\def\rootAtBottomFlag{Y}%
-}
-
-\def\rootAtTop{%
-    \global\def\rootAtBottomFlag{N}%
-}
-
-\def\resetRootPosition{%
-    \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag}
-}
-
-\def\alwaysRootAtBottom{%
-    \global\def\defaultRootAtBottomFlag{Y}
-    \rootAtBottom
-}
-
-\def\alwaysRootAtTop{%
-    \global\def\defaultRootAtBottomFlag{N}
-    \rootAtTop
-}
-
-

--- a/final_pre/dummy.tex	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-
-%%% jdummy.def
-%
-\DeclareRelationFont{JY1}{mc}{it}{}{OT1}{cmr}{it}{}
-\DeclareRelationFont{JT1}{mc}{it}{}{OT1}{cmr}{it}{}
-\DeclareFontShape{JY1}{mc}{m}{it}{<5> <6> <7> <8> <9> <10> sgen*min
-    <10.95><12><14.4><17.28><20.74><24.88> min10
-    <-> min10}{}
-\DeclareFontShape{JT1}{mc}{m}{it}{<5> <6> <7> <8> <9> <10> sgen*tmin
-    <10.95><12><14.4><17.28><20.74><24.88> tmin10
-    <-> tmin10}{}
-\DeclareRelationFont{JY1}{mc}{sl}{}{OT1}{cmr}{sl}{}
-\DeclareRelationFont{JT1}{mc}{sl}{}{OT1}{cmr}{sl}{}
-\DeclareFontShape{JY1}{mc}{m}{sl}{<5> <6> <7> <8> <9> <10> sgen*min
-    <10.95><12><14.4><17.28><20.74><24.88> min10
-    <-> min10}{}
-\DeclareFontShape{JT1}{mc}{m}{sl}{<5> <6> <7> <8> <9> <10> sgen*tmin
-    <10.95><12><14.4><17.28><20.74><24.88> tmin10
-    <-> tmin10}{}
-\DeclareRelationFont{JY1}{mc}{sc}{}{OT1}{cmr}{sc}{}
-\DeclareRelationFont{JT1}{mc}{sc}{}{OT1}{cmr}{sc}{}
-\DeclareFontShape{JY1}{mc}{m}{sc}{<5> <6> <7> <8> <9> <10> sgen*min
-    <10.95><12><14.4><17.28><20.74><24.88> min10
-    <-> min10}{}
-\DeclareFontShape{JT1}{mc}{m}{sc}{<5> <6> <7> <8> <9> <10> sgen*tmin
-    <10.95><12><14.4><17.28><20.74><24.88> tmin10
-    <-> tmin10}{}
-\DeclareRelationFont{JY1}{gt}{it}{}{OT1}{cmbx}{it}{}
-\DeclareRelationFont{JT1}{gt}{it}{}{OT1}{cmbx}{it}{}
-\DeclareFontShape{JY1}{mc}{bx}{it}{<5> <6> <7> <8> <9> <10> sgen*goth
-    <10.95><12><14.4><17.28><20.74><24.88> goth10
-    <-> goth10}{}
-\DeclareFontShape{JT1}{mc}{bx}{it}{<5> <6> <7> <8> <9> <10> sgen*tgoth
-    <10.95><12><14.4><17.28><20.74><24.88> tgoth10
-    <-> tgoth10}{}
-\DeclareRelationFont{JY1}{gt}{sl}{}{OT1}{cmbx}{sl}{}
-\DeclareRelationFont{JT1}{gt}{sl}{}{OT1}{cmbx}{sl}{}
-\DeclareFontShape{JY1}{mc}{bx}{sl}{<5> <6> <7> <8> <9> <10> sgen*goth
-    <10.95><12><14.4><17.28><20.74><24.88> goth10
-    <-> goth10}{}
-\DeclareFontShape{JT1}{mc}{bx}{sl}{<5> <6> <7> <8> <9> <10> sgen*tgoth
-    <10.95><12><14.4><17.28><20.74><24.88> tgoth10
-    <-> tgoth10}{}
-\DeclareRelationFont{JY1}{gt}{sc}{}{OT1}{cmbx}{sc}{}
-\DeclareRelationFont{JT1}{gt}{sc}{}{OT1}{cmbx}{sc}{}
-\DeclareFontShape{JY1}{mc}{bx}{sc}{<5> <6> <7> <8> <9> <10> sgen*goth
-    <10.95><12><14.4><17.28><20.74><24.88> goth10
-    <-> goth10}{}
-\DeclareFontShape{JT1}{mc}{bx}{sc}{<5> <6> <7> <8> <9> <10> sgen*tgoth
-    <10.95><12><14.4><17.28><20.74><24.88> tgoth10
-    <-> tgoth10}{}
-\DeclareRelationFont{JY1}{gt}{it}{}{OT1}{cmr}{it}{}
-\DeclareRelationFont{JT1}{gt}{it}{}{OT1}{cmr}{it}{}
-\DeclareFontShape{JY1}{gt}{m}{it}{<5> <6> <7> <8> <9> <10> sgen*goth
-    <10.95><12><14.4><17.28><20.74><24.88> goth10
-    <-> goth10}{}
-\DeclareFontShape{JT1}{gt}{m}{it}{<5> <6> <7> <8> <9> <10> sgen*tgoth
-    <10.95><12><14.4><17.28><20.74><24.88> tgoth10
-    <-> tgoth10}{}
-\endinput
-%%%% end of jdummy.def

--- a/final_pre/fancyhdr.sty	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-%%
-%% This is file `fancyhdr.sty',
-%% generated with the docstrip utility.
-%%
-%% The original source files were:
-%%
-%% fancyhdr.dtx  (with options: `fancyhdr')
-%% 
-%% This is a generated file.
-%% 
-%% This file may be distributed and/or modified under the conditions of
-%% the LaTeX Project Public License, either version 1.3 of this license
-%% or (at your option) any later version.  The latest version of this
-%% license is in:
-%% 
-%%    http://www.latex-project.org/lppl.txt
-%% 
-%% and version 1.3 or later is part of all distributions of LaTeX version
-%% 2005/12/01 or later.
-%% 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{fancyhdr}%
-           [2017/06/30 v3.9a
-                  Extensive control of page headers and footers]%
-% Copyright (C) 1994-2016 by Piet van Oostrum <piet@vanoostrum.org>
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\def\if@nch@mpty#1{\def\temp@a{#1}\ifx\temp@a\@empty}
-\def\f@nch@def#1#2{\if@nch@mpty{#2}\f@nch@gbl\def#1{\leavevmode}\else
-                                   \f@nch@gbl\def#1{#2\strut}\fi}
-\let\f@nch@gbl\global
-\def\f@nch@errmsg#1{%
-  \ifx\PackageError\undefined \errmessage{#1}\else
-  \PackageError{Fancyhdr}{#1}{}\fi}
-\def\f@nch@warning#1{%
-  \ifx\PackageWarning\undefined \errmessage{#1}\else
-  \PackageWarning{Fancyhdr}{#1}{}\fi}
-\def\f@nch@forc#1#2#3{\expandafter\f@rc\expandafter#1\expandafter{#2}{#3}}
-\def\f@rc#1#2#3{\def\temp@ty{#2}\ifx\@empty\temp@ty\else
-                                    \f@nch@rc#1#2\f@nch@rc{#3}\fi}
-\def\f@nch@rc#1#2#3\f@nch@rc#4{\def#1{#2}#4\f@rc#1{#3}{#4}}
-\newcommand{\f@nch@for}[3]{\edef\@fortmp{#2}%
-  \expandafter\@forloop#2,\@nil,\@nil\@@#1{#3}}
-\newcommand\f@nch@default[3]{%
-  \edef\temp@a{\lowercase{\edef\noexpand\temp@a{#3}}}\temp@a \def#1{}%
-  \f@nch@forc\tmpf@ra{#2}%
-  {\expandafter\f@nch@ifin\tmpf@ra\temp@a{\edef#1{#1\tmpf@ra}}{}}%
-  \ifx\@empty#1\def#1{#2}\fi}
-\newcommand{\f@nch@ifin}[4]{%
-  \edef\temp@a{#2}\def\temp@b##1#1##2\temp@b{\def\temp@b{##1}}%
-  \expandafter\temp@b#2#1\temp@b\ifx\temp@a\temp@b #4\else #3\fi}
-\newcommand{\fancyhead}[2][]{\f@nch@fancyhf\fancyhead h[#1]{#2}}%
-\newcommand{\fancyfoot}[2][]{\f@nch@fancyhf\fancyfoot f[#1]{#2}}%
-\newcommand{\fancyhf}[2][]{\f@nch@fancyhf\fancyhf {}[#1]{#2}}%
-\newcommand{\fancyheadoffset}[2][]{\f@nch@fancyhfoffs\fancyheadoffset h[#1]{#2}}%
-\newcommand{\fancyfootoffset}[2][]{\f@nch@fancyhfoffs\fancyfootoffset f[#1]{#2}}%
-\newcommand{\fancyhfoffset}[2][]{\f@nch@fancyhfoffs\fancyhfoffset {}[#1]{#2}}%
-\def\f@nch@fancyhf#1#2[#3]#4{%
-  \def\temp@c{}%
-  \f@nch@forc\tmpf@ra{#3}%
-  {\expandafter\f@nch@ifin\tmpf@ra{eolcrhf,EOLCRHF}%
-    {}{\edef\temp@c{\temp@c\tmpf@ra}}}%
-  \ifx\@empty\temp@c\else \f@nch@errmsg{Illegal char `\temp@c' in
-    \string#1 argument: [#3]}%
-  \fi \f@nch@for\temp@c{#3}%
-  {\f@nch@default\f@nch@@eo{eo}\temp@c \if@twoside\else \if\f@nch@@eo
-    e\f@nch@warning {\string#1's `E' option without twoside option is
-      useless}\fi\fi \f@nch@default\f@nch@@lcr{lcr}\temp@c
-    \f@nch@default\f@nch@@hf{hf}{#2\temp@c}%
-    \f@nch@forc\f@nch@eo\f@nch@@eo
-        {\f@nch@forc\f@nch@lcr\f@nch@@lcr
-          {\f@nch@forc\f@nch@hf\f@nch@@hf
-            {\expandafter\f@nch@def\csname
-              f@nch@\f@nch@eo\f@nch@lcr\f@nch@hf\endcsname {#4}}}}}}
-\def\f@nch@fancyhfoffs#1#2[#3]#4{%
-  \def\temp@c{}%
-  \f@nch@forc\tmpf@ra{#3}%
-  {\expandafter\f@nch@ifin\tmpf@ra{eolrhf,EOLRHF}%
-    {}{\edef\temp@c{\temp@c\tmpf@ra}}}%
-  \ifx\@empty\temp@c\else \f@nch@errmsg{Illegal char `\temp@c' in
-    \string#1 argument: [#3]}%
-  \fi \f@nch@for\temp@c{#3}%
-  {\f@nch@default\f@nch@@eo{eo}\temp@c \if@twoside\else \if\f@nch@@eo
-    e\f@nch@warning {\string#1's `E' option without twoside option is
-      useless}\fi\fi \f@nch@default\f@nch@@lcr{lr}\temp@c
-    \f@nch@default\f@nch@@hf{hf}{#2\temp@c}%
-    \f@nch@forc\f@nch@eo\f@nch@@eo
-        {\f@nch@forc\f@nch@lcr\f@nch@@lcr
-          {\f@nch@forc\f@nch@hf\f@nch@@hf
-            {\expandafter\setlength\csname
-              f@nch@O@\f@nch@eo\f@nch@lcr\f@nch@hf\endcsname {#4}}}}}%
-  \f@nch@setoffs}
-\newcommand{\lhead}[2][\f@nch@olh]%
-                     {\f@nch@def\f@nch@olh{#2}\f@nch@def\f@nch@elh{#1}}
-\newcommand{\chead}[2][\f@nch@och]%
-                     {\f@nch@def\f@nch@och{#2}\f@nch@def\f@nch@ech{#1}}
-\newcommand{\rhead}[2][\f@nch@orh]%
-                     {\f@nch@def\f@nch@orh{#2}\f@nch@def\f@nch@erh{#1}}
-\newcommand{\lfoot}[2][\f@nch@olf]%
-                     {\f@nch@def\f@nch@olf{#2}\f@nch@def\f@nch@elf{#1}}
-\newcommand{\cfoot}[2][\f@nch@ocf]%
-                     {\f@nch@def\f@nch@ocf{#2}\f@nch@def\f@nch@ecf{#1}}
-\newcommand{\rfoot}[2][\f@nch@orf]%
-                     {\f@nch@def\f@nch@orf{#2}\f@nch@def\f@nch@erf{#1}}
-\newlength{\f@nch@headwidth} \let\headwidth\f@nch@headwidth
-\newlength{\f@nch@O@elh}
-\newlength{\f@nch@O@erh}
-\newlength{\f@nch@O@olh}
-\newlength{\f@nch@O@orh}
-\newlength{\f@nch@O@elf}
-\newlength{\f@nch@O@erf}
-\newlength{\f@nch@O@olf}
-\newlength{\f@nch@O@orf}
-\newcommand{\headrulewidth}{0.4pt}
-\newcommand{\footrulewidth}{0pt}
-\@ifundefined{footruleskip}%
-      {\newcommand{\footruleskip}{.3\normalbaselineskip}}{}
-\newcommand{\plainheadrulewidth}{0pt}
-\newcommand{\plainfootrulewidth}{0pt}
-\newif\if@fancyplain \@fancyplainfalse
-\def\fancyplain#1#2{\if@fancyplain#1\else#2\fi}
-\headwidth=-123456789sp
-\let\f@nch@raggedleft\raggedleft
-\let\f@nch@raggedright\raggedright
-\let\f@nch@centering\centering
-\let\f@nch@everypar\everypar
-\def\f@nch@reset{\f@nch@everypar{}\restorecr\endlinechar=13
-  \let\\\@normalcr \let\raggedleft\f@nch@raggedleft
-  \let\raggedright\f@nch@raggedright \let\centering\f@nch@centering
-  \def\baselinestretch{1}%
-  \hsize=\headwidth
-  \def\nouppercase##1{{\let\uppercase\relax\let\MakeUppercase\relax
-      \expandafter\let\csname MakeUppercase \endcsname\relax##1}}%
-  \ifx\undefined\@newbaseline % NFSS not present; 2.09 or 2e
-  \ifx\@normalsize\undefined \normalsize % for ucthesis.cls
-  \else \@normalsize \fi \else % NFSS (2.09) present
-  \@newbaseline%
-  \fi}
-\fancyhf{}
-\if@twoside
-  \fancyhead[el,or]{\fancyplain{}{\slshape\rightmark}}
-  \fancyhead[er,ol]{\fancyplain{}{\slshape\leftmark}}
-\else
-  \fancyhead[l]{\fancyplain{}{\slshape\rightmark}}
-  \fancyhead[r]{\fancyplain{}{\slshape\leftmark}}
-\fi
-\fancyfoot[c]{\rmfamily\thepage} % page number
-\def\f@nch@vbox#1#2{\setbox0\vbox{#2}\ifdim\ht0>#1\f@nch@warning
-  {\string#1 is too small (\the#1): ^^J Make it at least \the\ht0.^^J We
-    now make it that large for the rest of the document.^^J This may
-    cause the page layout to be inconsistent, however\@gobble}%
-  \dimen0=#1\global\setlength{#1}{\ht0}\ht0=\dimen0\fi \box0}
-\def\f@nch@head#1#2#3#4#5{#1\hbox to\headwidth{\f@nch@reset
-    \f@nch@vbox\headheight{\hbox
-      {\rlap{\parbox[b]{\headwidth}{\raggedright#2}}\hfill
-        \parbox[b]{\headwidth}{\centering#3}\hfill
-        \llap{\parbox[b]{\headwidth}{\raggedleft#4}}}\headrule}}#5}
-\def\f@nch@foot#1#2#3#4#5{#1\hbox to\headwidth{\f@nch@reset
-    \f@nch@vbox\footskip{\footrule
-      \hbox{\rlap{\parbox[t]{\headwidth}{\raggedright#2}}\hfill
-        \parbox[t]{\headwidth}{\centering#3}\hfill
-        \llap{\parbox[t]{\headwidth}{\raggedleft#4}}}}}#5}
-\def\headrule{{\if@fancyplain\let\headrulewidth\plainheadrulewidth\fi
-    \hrule\@height\headrulewidth\@width\headwidth
-    \vskip-\headrulewidth}}
-\def\footrule{{\if@fancyplain\let\footrulewidth\plainfootrulewidth\fi
-    \vskip-\footruleskip\vskip-\footrulewidth
-    \hrule\@width\headwidth\@height\footrulewidth\vskip\footruleskip}}
-\def\ps@fancy{%
-  \@ifundefined{@chapapp}{\let\@chapapp\chaptername}{}% for amsbook
-\@ifundefined{MakeUppercase}{\def\MakeUppercase{\uppercase}}{}%
-\ifx\chapter\@undefined \def\sectionmark##1{\markboth
-  {\MakeUppercase{\ifnum \c@secnumdepth>\z@ \thesection\hskip 1em\relax
-      \fi ##1}}{}}%
-\def\subsectionmark##1{\markright {\ifnum \c@secnumdepth >\@ne
-    \thesubsection\hskip 1em\relax \fi ##1}}%
-\else \def\chaptermark##1{\markboth {\MakeUppercase{\ifnum
-      \c@secnumdepth>\m@ne \@chapapp\ \thechapter. \ \fi ##1}}{}}%
-\def\sectionmark##1{\markright{\MakeUppercase{\ifnum \c@secnumdepth >\z@
-      \thesection. \ \fi ##1}}}%
-\fi
-\ps@@fancy
-\gdef\ps@fancy{\@fancyplainfalse\ps@@fancy}%
-\ifdim\headwidth<0sp
-    \global\advance\headwidth123456789sp\global\advance\headwidth\textwidth
-\fi}
-\def\ps@fancyplain{\ps@fancy \let\ps@plain\ps@plain@fancy}
-\def\ps@plain@fancy{\@fancyplaintrue\ps@@fancy}
-\let\ps@@empty\ps@empty
-\def\ps@@fancy{%
-  \ps@@empty
-  \def\@mkboth{\protect\markboth}%
-  \def\@oddhead{\f@nch@head\f@nch@Oolh\f@nch@olh\f@nch@och\f@nch@orh\f@nch@Oorh}%
-  \def\@oddfoot{\f@nch@foot\f@nch@Oolf\f@nch@olf\f@nch@ocf\f@nch@orf\f@nch@Oorf}%
-  \def\@evenhead{\f@nch@head\f@nch@Oelh\f@nch@elh\f@nch@ech\f@nch@erh\f@nch@Oerh}%
-  \def\@evenfoot{\f@nch@foot\f@nch@Oelf\f@nch@elf\f@nch@ecf\f@nch@erf\f@nch@Oerf}%
-}
-\def\f@nch@Oolh{\if@reversemargin\hss\else\relax\fi}
-\def\f@nch@Oorh{\if@reversemargin\relax\else\hss\fi}
-\let\f@nch@Oelh\f@nch@Oorh
-\let\f@nch@Oerh\f@nch@Oolh
-\let\f@nch@Oolf\f@nch@Oolh
-\let\f@nch@Oorf\f@nch@Oorh
-\let\f@nch@Oelf\f@nch@Oelh
-\let\f@nch@Oerf\f@nch@Oerh
-\def\f@nch@offsolh{\headwidth=\textwidth\advance\headwidth\f@nch@O@olh
-                   \advance\headwidth\f@nch@O@orh\hskip-\f@nch@O@olh}
-\def\f@nch@offselh{\headwidth=\textwidth\advance\headwidth\f@nch@O@elh
-                   \advance\headwidth\f@nch@O@erh\hskip-\f@nch@O@elh}
-\def\f@nch@offsolf{\headwidth=\textwidth\advance\headwidth\f@nch@O@olf
-                   \advance\headwidth\f@nch@O@orf\hskip-\f@nch@O@olf}
-\def\f@nch@offself{\headwidth=\textwidth\advance\headwidth\f@nch@O@elf
-                   \advance\headwidth\f@nch@O@erf\hskip-\f@nch@O@elf}
-\def\f@nch@setoffs{%
-  \f@nch@gbl\let\headwidth\f@nch@headwidth
-  \f@nch@gbl\let\f@nch@Oolh\f@nch@offsolh
-  \f@nch@gbl\let\f@nch@Oelh\f@nch@offselh \f@nch@gbl\let\f@nch@Oorh\hss
-  \f@nch@gbl\let\f@nch@Oerh\hss \f@nch@gbl\let\f@nch@Oolf\f@nch@offsolf
-  \f@nch@gbl\let\f@nch@Oelf\f@nch@offself \f@nch@gbl\let\f@nch@Oorf\hss
-  \f@nch@gbl\let\f@nch@Oerf\hss
-}
-\newif\iff@nch@footnote
-\AtBeginDocument{%
-  \let\latex@makecol\@makecol
-  \def\@makecol{\ifvoid\footins\f@nch@footnotefalse\else\f@nch@footnotetrue\fi
-    \let\topfloat\@toplist\let\botfloat\@botlist\latex@makecol}%
-}
-\newcommand\iftopfloat[2]{\ifx\topfloat\empty #2\else #1\fi}%
-\newcommand\ifbotfloat[2]{\ifx\botfloat\empty #2\else #1\fi}%
-\newcommand\iffloatpage[2]{\if@fcolmade #1\else #2\fi}%
-\newcommand\iffootnote[2]{\iff@nch@footnote #1\else #2\fi}%
-\newcommand{\fancypagestyle}[2]{%
-  \@namedef{ps@#1}{\let\f@nch@gbl\relax#2\relax\ps@fancy}}
-\endinput
-%%
-%% End of file `fancyhdr.sty'.

Binary file final_pre/fig/goto.pdf has changed

Binary file final_pre/finalPre.pdf has changed

--- a/final_pre/finalPre.tex	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-\documentclass[twocolumn,twoside,9.5pt]{jarticle}
-\usepackage[dvipdfmx]{graphicx}
-\usepackage{picins}
-\usepackage{fancyhdr}
-%\pagestyle{fancy}
-\usepackage{abstract}
-\usepackage{url}
-\usepackage{bussproofs}
-\usepackage{listings,jlisting}
-\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
-\rhead{}
-\cfoot{}
-
-\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
-\setlength{\headheight}{0mm}
-\setlength{\headsep}{5mm}
-\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
-\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
-\setlength{\textwidth}{181mm}
-\setlength{\textheight}{261mm}
-\setlength{\footskip}{0mm}
-\pagestyle{empty}
-
-\lstset{
-  frame=single,
-  keepspaces=true,
-  breaklines=true,
-  xleftmargin=0zw,
-  xrightmargin=0zw,
-  framerule=.2pt,
-  columns=[l]{fullflexible},
-  language={},
-  tabsize=4,
-  lineskip=-0.5zw,
-  escapechar={@},
-}
-
-
-\input{dummy.tex}
-\renewcommand{\abstractname}{Abstract}
-\begin{document}
-
-\title{Agda と継続を用いたプログラムの検証 \\ Verification of program using Continuation by Agda}
-\author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
-\date{}
-\twocolumn [
-\maketitle
-\begin{onecolabstract}
-
-  % 高い信頼性を持つことは重要である。  
-  % 私たちはプログラムの信頼性を高めるためにCodeGear、DataGearという単位でプログラ
-  % ムを書くことを提案している。
-  % そのためにCodeGear、DataGearという単位を使える言語 CbC を開発している。
-  % CbC では既存の実装でのデータの取扱が複雑になっている。
-  % そのためにDataGearとCodeGearを Interface という単位でまとめた。
-  % これら単位をAgdaでも使えるようにし、CbC で記述した Stackや Tree を Agda に
-  % 変換した。
-  % この論文ではそれらに対して幾つかの部分的な証明を試みた。
-
-  
-  High reliability is important in Program.
-  we are proposing programing units of CodeGear, DataGear for increase
-  the reliability.
-  we are deceloping Continuation based C (CbC) that can use units CodeGear and
-  DataGear.
-  In CbC, the handling of data in existing implementations is complicated.
-  for that purpose, we can provide a interface mechanisms which are packages of
-  CodeGears and DataGears.
-  we made these units and interface available for Agda.
-  In this papaer, we converted Stack and Tree using the interface discribe in
-  CbC to Agda, and we tried several proofs on them.
-  
-
-\end{onecolabstract}]
-\thispagestyle{fancy}
-
-% ソフトウェアの信頼性の保証
-% 　　CbC の話(CG,DGの話も)
-% 　　メタ計算を分けてる
-%    context (Meta DataGear)
-%    そのために interface
-%    Agda でも interfece を実装して検証した
-
-\section{ソフトウェアの信頼性の保証}
-ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証す
-る方法として代表的なものはモデル検査と、定理証明が存在している。定理証明支援器と
-して有名なものとしては Agda\cite{agda} が存在する。
-
-当研究室では検証しやすいプログラムの単位として、 CodeGear と DataGear という単位
-を用いるプログラミングスタイルを提案している。
-また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語として
-Countinuation based C (以下 CbC) を開発している。
-% 本研究では、検証や証明に直接使用できる言語として CbC を用いる。
-
-CbC では通常の計算とメタ計算を分けて記述している。
-しかし、CodeGear で DataGear を扱う際、 Context と呼ばれる CodeGear、 DataGear の
-リスト等を持っている Meta DataGear を経由する。
-通常の CodeGear から Meta DataGear である Context を直接扱えると、ユーザーがメタ
-計算をノーマルレベルで自由に記述できてしまい、信頼性を損なう。そのため、 CbC
-では Context を通して、次の CodeGear に接続する Meta CodeGear である stub
- CodeGear を定義している。
-
-CbC で実装していくにつれて特殊な stub CodeGear の記述が複雑になった。
-そこで既存の実装をモジュールとして扱うために Interface という仕組みを導入した。
-Interface では、DataGear に対しての操作(API)を CodeGear とその CodeGear で扱われ
-ている DataGearの集合を抽象的に表現した Meta DataGear として定義されている。
-
-本研究では CbCで使われている Interface を含めて証明を行うために、 Agda 上で
-Interface の定義、実装を行なった。
-また Interface を含めた Stack と Tree の部分的な証明を行なった。
-
-\section{Countinuation based C (CbC)}
-Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。
-CbC は C 言語とほぼおなじ構文を持つが、 C の関数の代わりに CodeGear を用いて処理
-を記述する。
-CodeGear は関数定義の先頭に $\_\_code$ をつけて定義する。
-CodeGear は処理の単位でそれらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。
-DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。
-CbC ではこの継続処理がメタ計算として定義されており、通常計算である CodeGear を変
-更することなく検証や資源管理等の記述を行うことができる。
-例として CbC の簡単な例をソースコード\ref{src:goto}に、流れを図\ref{fig:code_simple}示す。
-
-\lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc}
-
-\begin{figure}[htpb]
- \begin{center}
-   \scalebox{0.7}[0.7]{\includegraphics{fig/codesegment.pdf}}
- \end{center}
- \caption{ソースコード\ref{src:goto}の流れ}
- \label{fig:code_simple}
-\end{figure}
-
-ソースコード\ref{src:goto}では　cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、
-cs1 の Input DataGear になる。
-流れ\ref{fig:code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
-続に指定された CodeGear へ継続する。
-
-\section{Agda}
-Agda とは定理証明支援器であり依存型を関数プログラミング言語である。
-依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
-CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数
-として定義できる。
-ソースコード\ref{src:goto} で示した CbC の簡単な例を Agda に変換したものをソースコー
-ド\ref{src:agda-css}に示す。
-
-\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義]
-{src/CodeSegments.agda}
-
-Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。
-関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて
-記述する。
-DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で
-ある。
- % 定義をする際は record キーワードのあとにレコード名、
-% 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
-% ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
-% していく。複数の値を列挙する際は ; で区切る。
-% Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す
-% \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
-このように CbC のコードを Agda に変換し、証明を行う。
-
-\section{CbC における Interface の定義}
-CbC で実装していくにつれ、stub CodeGear の記述が煩雑になった。
-そのため 既存の実装を モジュールとして扱うため Interface を導入した。
-Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
-CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
-として定義した。例として Stack での Interface の実装(ソースコード\ref{src:interface})を示す。
-
-\lstinputlisting[label=src:interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}
-
-元の実装の push では Stack を指定する必要があるが、
-Interface での実装は push 先の Stack が stackImpl として扱
-われている。この stackImpl は呼ばれた時の Stack と同じになる。
-これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。
-このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
-しが容易になる。
-
-
-\section{Agda における Interface の定義、実装}
-Agda でも CbC と同様に Interface の定義、実装した。
-例として Agda で実装した Stack-interface の一部をみる。
-Stack の定義はソースコード\ref{src:agda-interface}、実装は ソースコード
-\ref{src:agda-single-linked-stack}
-として書かれている。それを Stack 側から interface を通して呼び出している。
-
-\lstinputlisting[label=src:agda-interface, caption=Agda における Stack
--Interface の定義の一部] {src/AgdaInterface.agda}
-
-\lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack
--Interface の実装の一部] {src/AgdaSingleLinkedStack.agda}
-
-\section{Agda による Interface 部分を含めた Stack の部分的な証明}
-今回は Interface を通した Stack で push
-、 pop などの操作が正しく行われるかの証明を行った。
-ここでの証明とは Stack が特定の性質を持つことを保証することである。
-
-Stack の処理として様々な性質が存在するが、ここでは
-「どのような状態の Stack でも、値を push した後 pop した値は直前
-に入れた値と一致する」という性質を証明した。
-
-まず始めに不定状態の Stack をソースコード~\ref{src:agda-in-some-state}
-で定義した。 stackInSomeState は不定状態の Stack を定義する関数である。
-ソースコード~\ref{src:agda-proof}の証明ではこの stackInSomeState に対し
-て、 push を2回行い、 pop2 をして取れたデータは push したデータと同じものになる
-ことの証明している。
-
- \lstinputlisting[label=src:agda-in-some-state, caption=不定なStackの定義]{src/AgdaStackSomeState.agda}
-
- \lstinputlisting[label=src:agda-proof, caption=push$->$push$->$pop2 の証明]{src/AgdaProof.agda}
- 
-stackInSomeState は引数として s を取っていて、不定な Stack そこに x 、 y の２つのデー
-タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
-Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
-型に書いた。関数本体で返る値は$ x \equiv x1 と y \equiv y1$で両方共に成り立つ為、
- refl で推論が通る。
-これにより、抽象化した Stack に対して push を2回行い、 pop を行うと push したものと同じも
-のを受け取れることが証明できた。
- 
-\section{まとめ}
-本研究では CodeGear、 DataGear を用いたプログラミング手法を用いて、Agda で
-Interface を用いたプログラムを実装、検証した。
-また、 CbC で記述した時には細かく分かっていなかった Interface の型が明確に
-なった。
-今後の課題としては、Tree 側では証明が複雑化し、うまく証明できていないことと、
-Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare
-Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。
-
-\nocite{*}
-\bibliographystyle{junsrt}
-\bibliography{reference}
-\end{document}

--- a/final_pre/jlisting.sty	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,216 +0,0 @@
-\NeedsTeXFormat{LaTeX2e}
-\def\filedate{2006/02/20}
-\def\fileversion{0.2}
-\ProvidesPackage{jlisting}[\filedate\space\fileversion\space(Thor)]
-%
-\newcount\lst@nextchar
-\let\lst@@ProcessSpace\lst@ProcessSpace
-\def\lst@ProcessSpace#1{%
-   \lst@check@chartype{#1}%
-      \lst@@ProcessSpace
-      \lst@whitespacetrue}
-\let\lst@@ProcessLetter\lst@ProcessLetter
-\def\lst@ProcessLetter#1#2{%
-   \lst@check@chartype{#2}%
-      {\lst@@ProcessLetter{#1}}%
-      \relax}
-\let\lst@@ProcessDigit\lst@ProcessDigit
-\def\lst@ProcessDigit#1#2{%
-   \lst@check@chartype{#2}%
-      {\lst@@ProcessDigit{#1}}%
-      \relax}
-\let\lst@@ProcessOther\lst@ProcessOther
-\def\lst@ProcessOther#1#2{%
-   \lst@check@chartype{#2}%
-      {\lst@@ProcessOther{#1}}%
-      \relax}
-\let\lst@@ProcessTabulator\lst@ProcessTabulator
-\def\lst@ProcessTabulator#1{%
-   \lst@check@chartype{#1}%
-      \lst@@ProcessTabulator
-      \relax}
-\def\lst@check@chartype#1#2#3{%
-   \edef\@tempa{\lst@nextchar=`\string#1\relax}%
-   \afterassignment\remove@to@nnil
-   \@tempa\@nnil
-   #2%
-   \ifnum\lst@nextchar<\@cclvi
-      #3%
-   \else
-      \lst@ifletter \else \lst@OutputOther \fi
-      \lst@whitespacefalse
-      \expandafter\lst@AppendJchar
-   \fi
-   #1}
-\def\lst@AppendJchar#1#2{%
-   \lst@check@chartype{#2}%
-      {\advance\lst@length\@ne\lst@Append{#1}}%
-      \relax}
-\def\lst@check@chartype@BOL#1{%
-   \edef\@tempa{\lst@nextchar=`\string#1\relax}%
-   \afterassignment\remove@to@nnil
-   \@tempa\@nnil
-   \ifnum\lst@nextchar<\@cclvi\else
-      \lst@whitespacefalse
-      \expandafter\lst@AppendJchar
-   \fi
-   #1}
-\def\lst@InputListing#1{%
-   \begingroup
-      \lsthk@PreSet \gdef\lst@intname{#1}%
-      \expandafter\lstset\expandafter{\lst@set}%
-      \lsthk@DisplayStyle
-      \catcode\active=\active
-      \lst@Init\relax \let\lst@gobble\z@
-      \lst@SkipToFirst
-      \lst@ifprint \def\lst@next{\lst@get@filecontents{#1}}%
-      \else        \let\lst@next\@empty
-      \fi
-      \lst@next
-      \lst@DeInit
-   \endgroup}
-\newread\lst@inputfile
-\def\lst@get@filecontents#1{%
-   \let\lst@filecontents\@empty
-   \openin\lst@inputfile=#1\relax
-   \let\@lst@get@filecontents@prevline\relax
-   \lst@get@filecontents@loop
-   \closein\lst@inputfile
-   \lst@filecontents\empty}
-\def\lst@get@filecontents@loop{%
-   \read\lst@inputfile to\@lst@get@filecontents@currline
-   \ifx\@lst@get@filecontents@prevline\relax\else
-      \expandafter\expandafter\expandafter\def
-      \expandafter\expandafter\expandafter\lst@filecontents
-      \expandafter\expandafter\expandafter{%
-         \expandafter\lst@filecontents\@lst@get@filecontents@prevline}%
-   \fi
-   \let\@lst@get@filecontents@prevline\@lst@get@filecontents@currline
-   \ifeof\lst@inputfile\else
-      \expandafter\lst@get@filecontents@loop
-   \fi}
-%%% [$B$3$N=hM}$b!$AjEv6/0z$G$9!%(B]
-\def\lst@BOLGobble{%
-   \ifnum\lst@gobble>\z@
-      \@tempcnta\lst@gobble\relax
-      \expandafter\lst@BOLGobble@
-   \else
-      \expandafter\lst@check@chartype@BOL
-   \fi}
-\def\lst@BOLGobble@#1{%
-   \let\lst@next#1%
-   \ifx \lst@next\relax\else
-   \ifx \lst@next\lst@MProcessListing\else
-   \ifx \lst@next\lst@ProcessFormFeed\else
-   \ifx \lst@next\lstenv@backslash
-      \let\lst@next\lstenv@BOLGobble@@
-   \else
-      \let\lst@next\lst@BOLGobble@@
-      \ifx #1\lst@ProcessTabulator
-         \advance\@tempcnta-\lst@tabsize\relax
-         \ifnum\@tempcnta<\z@
-            \lst@length-\@tempcnta \lst@PreGotoTabStop
-         \fi
-      \else
-         \edef\@tempa{\lst@nextchar=`\string#1\relax}%
-         \@tempa
-         \ifnum\lst@nextchar<\@cclvi\else
-            \advance\@tempcnta\m@ne
-         \fi
-         \advance\@tempcnta\m@ne
-      \fi
-   \fi \fi \fi \fi
-   \lst@next}
-\def\lst@BOLGobble@@{%
-   \ifnum\@tempcnta>\z@
-      \expandafter\lst@BOLGobble@
-   \else
-      \expandafter\lst@check@chartype@BOL
-   \fi
-}
-%
-%    \begin{$B=$@5;v9`(B}{1.3}
-% $B$A$g$C$H$7$?=$@5(B
-\gdef\lst@breakProcessOther#1{\lst@ProcessOther#1}
-% $B%=!<%9%3!<%IL\<!$K$*$1$kJ8;z$HHV9f$N6u$-(B
-\let \l@lstlisting = \l@figure
-% $B%-%c%W%7%g%s$H%=!<%9%3!<%IL\<!$KBP$9$kF|K\8lBP1~(B
-\def\lstlistingname{$B%=!<%9%3!<%I(B}
-\def\lstlistlistingname{$B%=!<%9%3!<%IL\<!(B}
-%    \end{$B=$@5;v9`(B}
-\endinput
-% 
-%#!platex
-\documentclass[papersize]{jsarticle}
-% Macros
-\IfFileExists{dvipdfmx.def}{%
-  \usepackage[dvipdfmx]{color,graphicx}%
-}{%
-  \usepackage[dvipdfm]{color,graphicx}%
-}
-\usepackage{listings}[2004/09/07]
-\usepackage{jlisting}[2006/02/20]
-\usepackage{url} 
-\usepackage{verbatim}
-
-\makeatletter
-% Original Macros
-\def\email#1{\gdef\@email{\texttt{#1}}}
-\def\homepage#1{\gdef\@homepage{\texttt{#1}}}
-\def\mac#1{\textsf{#1}}
-\def\URL#1{\texttt{#1}}
-\def\src#1{\texttt{#1}}
-
-% Dvipdfmx.def 
-\def\dvipdfmxDefi{http://tex.dante.jp/ok/dvipdfmx/}
-\def\dvipdfmxDefii{http://ftp.ktug.or.kr/KTUG/dvipdfmx/contrib/latex/}
-
-\IfFileExists{dvipdfmx.def}{%
-   \let \IfDvipdfmxDef = \empty \relax}{%
-   \typeout{^^Jget dvipdfmx.def at \dvipdfmxDefi^^J
-            or \dvipdfmxDefii^^J}%
-   \def\IfDvipdfmxDef{Get \src{dvipdfmx.def} at \URL \dvipdfmxDefii \\ 
-      or \URL \dvipdfmxDefi.}%
-}
-
-% Author Info
-\author   {Th\'or Watanabe\thanks \@email \space \thanks \@homepage}
-\title    {\mac{jlisting.sty}\\
-          ---Japanese Localized Patch File of \mac{listings}---}
-\email    {thor@tex.dante.jp}
-\homepage {http://tex.dante.jp/typo/}
-\date     {2006/02/20}
-
-\makeatother
-
-\begin{document}
-\maketitle
-%\IfDvipdfmxDef
-
-\section{$B$A$g$C$H$7$?@bL@(B}% Short Description
- 
-$B1|B<@2I';a$N7G<(HD$N!VHFMQE*$JIbF0BN!W$H$$$&0lO"$N=q$-9~$_$+$i(B
-$BE>:\$7$^$7$?!#(B
-
-\begin{quote}
- \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21172.html}\\
- \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21184.html}\\
- \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21189.html}\\
- \url{http://http://cise.edu.mie-u.ac.jp/~okumura/texfaq/qa/21197.html}
-\end{quote}
-
- Copyright $B$O5H1JE/H~;a$K$"$k$N$@$H;W$$$^$9!%(B
- 
-\section{$B99?7MzNr(B}% ChageLogs
-
-\begin{description}
- \item[ver.~0.1 (2004/03/24)]
-   $B$H$j$"$($:8x3+!%(B
- \item[ver.~0.2 (2006/02/20)] 
-   \verb|\lst@breakProcessOther| $BL?Na$NDj5A$NDI2C!%(B
-\end{description}
-
-\section{$B%=!<%9%3!<%I(B}
-\par\narrowbaselines
-\verbatiminput{jlisting.sty}
-\end{document}

--- a/final_pre/modus-ponens/Makefile	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-# Settings
-TARGET=modus-ponens
-BIBTEX=echo # pbibtex
-BB=extractbb
-
-vpath pdf fig
-FIGURES=$(wildcard fig/*.pdf)
-FIGURES_FOR_TEX=$(subst .pdf,.xbb,$(FIGURES))
-
-# dependencies
-$(TARGET).pdf : $(TARGET).dvi
-	dvipdfmx $<
-
-$(TARGET).dvi : $(wildcard *.tex) $(FIGURES_FOR_TEX) $(SOURCES_FOR_TEX)
-	platex  $(TARGET).tex
-	$(BIBTEX) $(TARGET)
-	platex  $(TARGET).tex
-	platex  $(TARGET).tex
-
-%.xbb: %.pdf
-	$(BB) $<
-
-
-# commands
-.PHONY : clean all open remake
-
-clean:
-	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg
-
-all: $(TARGET).pdf
-
-open: $(TARGET).pdf
-	open $(TARGET).pdf
-
-remake:
-	make clean
-	make all

--- a/final_pre/modus-ponens/bussproofs.sty	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1136 +0,0 @@
-%
-\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
-% bussproofs.sty.  Version 1.1
-%     (c) 1994,1995,1996,2004,2005,2006, 2011. 
-%     Copyright retained by Samuel R. Buss.
-%
-% ==== Legal statement: ====
-% This work may be distributed and/or modified under the
-% conditions of the LaTeX Project Public License, either version 1.3
-% of this license or (at your option) any later version.
-% The latest version of this license is in
-%  http://www.latex-project.org/lppl.txt.
-% and version 1.3 or later is part of all distributions of LaTeX
-% version 2005/12/1 or later.
-%
-% This work has the LPPL maintenance status 'maintained'.
-%
-% The Current Maintainer of the work is Sam Buss.
-%
-% This work consists of bussproofs.sty.
-%  =====
-% Informal summary of legal situation:
-%     This software may be used and distributed freely, except that
-%     if you make changes, you must change the file name to be different
-%     than bussproofs.sty to avoid compatibility problems.
-% The terms of the LaTeX Public License are the legally controlling terms
-%     and override any contradictory terms of the "informal situation".
-%
-%     Please report comments and bugs to sbuss@ucsd.edu.
-%
-%  Thanks to Felix Joachimski for making changes to let these macros
-%   work in plain TeX in addition to LaTeX.  Nothing has been done
-%   to see if they work in AMSTeX.  The comments below mostly
-%   are written for LaTeX, however.
-%  July 2004, version 0.7
-%       - bug fix, right labels with descenders inserted too much space.
-%         Thanks to Peter Smith for finding this bug,
-%     see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
-%  March 2005, version 0.8.
-%   Added a default definition for \fCenter at Denis Kosygin's
-%   suggestion.
-%  September 2005, version 0.9.
-%       Fixed some subtle spacing problems, by adding %'s to the end of
-%   few lines where they were inadvertantly omitted.  Thanks to
-%   Arnold Beckmann for finding and fixing this problem.
-%  April 2006, version 0.9.1.  Updated comments and testbp2.tex file.
-%       No change to the actual macros.
-%  June 2006, version 1.0.  The first integer numbered release.
-%       New feature: root of proof may now be at the bottom instead of
-%       at just the top.  Thanks to Alex Hertel for the suggestion to implement
-%       this.
-%  June 2011, version 1.1.  
-%       New feature: 4-ary and 5-ary inferences.  Thanks to Thomas Strathmann
-%       for taking the initiative to implement these.
-%         Four new commands: QuaternaryInf(C) and QuinaryInf(C).
-%       Bug fix: \insertBetweenHyps now works for proofs with root at top and
-%            three or more hypotheses..
-
-% A good exposition of how to use bussproofs.sty (version 0.9) has been written
-%  by Peter Smith and is available on the internet.
-% The comments below also describe the features of bussproofs.sty,
-%  including user-modifiable parameters.
-
-%  bussproofs.sty allows the construction of proof trees in the
-%     style of the sequent calculus and many other proof systems
-%     One novel feature of these macros is they support the horizontal
-%     alignment according to some center point specified with the
-%     command \fCenter.  This is the style often used in sequent
-%     calculus proofs.
-%     Proofs are specified in left-to-right traversal order.
-%       For example a proof
-%               A   B
-%                               -----
-%                          D      C
-%                         ---------
-%                             E
-%
-%     if given in the order D,A,B,C,E.  Each line in the proof is
-%     specified according to the arity of the inference which generates
-%     it.  Thus, E would be specified with a \BinaryInf  or  \BinaryInfC
-%     command.
-%
-%     The above proof tree could be displayed with the commands:
-%
-%               \AxiomC{D}
-%               \AxiomC{A}
-%               \AxiomC{B}
-%               \BinaryInfC{C}
-%               \BinaryInfC{E}
-%               \DisplayProof
-%
-%     Inferences in a proof may be nullary (axioms), unary, binary, or
-%     trinary.
-%
-%     IMPORTANT:  You must give the \DisplayProof command to make the proof
-%      be printed.  To display a centered proof on a line by itself,
-%      put the proof inside \begin{center} ... \end{center}.
-%
-%     There are two styles for specifying horizontal centering of
-%     lines (formulas or sequents) in a proof.  One format \AxiomC{...}
-%     just centers the formula {...} in the usual way.  The other
-%     format is \Axiom$...\fCenter...$.  Here,  the \fCenter specifies
-%     the center of the formula.  (It is permissable for \fCenter to
-%     generate typeset material; in fact, I usually define it to generate
-%     the sequent arrow.)  In unary inferences, the \fCenter
-%     positions will be vertically aligned in the upper and lower lines of
-%     the inference.  Unary, Binary, Trinary inferences are specified
-%     with the same format as Axioms.  The two styles of centering
-%     lines may be combined in a single proof.
-%
-%     By using the optional \EnableBpAbbreviations command, various
-%   abbreviated two or three letter commands are enabled.  This allows,
-%   in particular:
-%   \AX and \AXC for \Axiom and \AxiomC, (resp.),
-%   \DP for \DisplayProof,
-%   \BI and \BIC for \BinaryInf and \BinaryInfC,
-%   \UI and \UIC for \UnaryInf  and \UnaryInfC,
-%   \TI and \TIC for \TrinaryInf and \TrinaryInfC,
-%   \LL and \RL for \LeftLabel and \RightLabel.
-%   See the source code below for additional abbreviations.
-%     The enabling of these short abbreviations is OPTIONAL, since
-%       there is the possibility of conflicting with names from other
-%       macro packages.
-%
-%     By default, the inferences have single horizontal lines (scores)
-%       This can be overridden using the \doubleLine, \noLine commands.
-%       These two commands affect only the next inference.  You can make
-%   make a permanent override that applies to the rest of the current
-%       proof using \alwaysDoubleLine and \alwaysNoLine.  \singleLine
-%   and \alwaysSingleLine work in the analogous way.
-%
-%     The macros do their best to give good placements of for the
-%     parts of the proof.  Several macros allow you to override the
-%     defaults.  These are \insertBetweenHyps{...} which overrides
-%     the default spacing between hypotheses of Binary and Trinary
-%     inferences with {...}.  And \kernHyps{...} specifies a distance
-%     to shift the whole block of hypotheses to the right (modifying
-%     the default center position.
-%       Other macros set the vertical placement of the whole proof.
-%     The default is to try to do a good job of placement for inferences
-%     included in text.  Two other useful macros are: \bottomAlignProof
-%     which aligns the hbox output by \DisplayProof according to the base
-%     of the bottom line of the proof, and \centerAlignProof which
-%     does a precise center vertical alignment.
-%
-%     Often, one wishes to place a label next to an inference, usually
-%   to specify the type of inference.  These labels can be placed
-%       by using the commands \LeftLabel{...} and \RightLabel{...}
-%       immediately before the command which specifies the inference.
-%       For example, to generate
-%
-%                       A     B
-%                      --------- X
-%                          C
-%
-%       use the commands
-%             \AxiomC{A}
-%             \AxiomC{B}
-%             \RightLabel{X}
-%             \BinaryInfC{C}
-%             \DisplayProof
-%
-%     The \DisplayProof command just displays the proof as a text
-%   item.  This allows you to put proofs anywhere normal text
-%   might appear; for example, in a paragraph, in a table, in
-%   a tabbing environment, etc.  When displaying a proof as inline text,
-%   you should write \DisplayProof{}  (with curly brackets) so that
-%   LaTeX will not "eat" the white space following the \DisplayProof
-%   command.
-%     For displaying proofs in a centered display:  Do not use the \[...\]
-%   construction (nor $$...$$).  Instead use
-%   \begin{center} ... \DisplayProof\end{center}.
-%     Actually there is a better construction to use instead of the
-%   \begin{center}...\DisplayProof\end{center}.  This is to
-%   write
-%       \begin{prooftree} ... \end{prooftree}.
-%       Note there is no \DisplayProof used for this: the
-%   \end{prooftree} automatically supplies the \DisplayProof
-%   command.
-%
-%     Warning: Any commands that set line types or set vertical or
-%   horizontal alignment that are given AFTER the \DisplayProof
-%   command will affect the next proof, no matter how distant.
-
-
-
-
-% Usages:
-% =======
-%
-%   \Axiom$<antecedent>\fCenter<succedent>$
-%
-%   \AxiomC{<whole sequent or formula}
-%
-%   Note that the use of surrounding {}'s is mandatory in \AxiomC and
-%   is prohibited in $\Axiom.  On the other hand, the $'s are optional
-%   in \AxiomC and are mandatory in \Axiom.  To typeset the argument
-%   to \AxiomC in math mode, you must use $'s (or \(...\) ).
-%   The same comments apply to the inference commands below.
-%
-%   \UnaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \UnaryInfC{<whole sequent or formula>}
-%
-%   \BinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \BinaryInfC{<whole sequent or formula>}
-%
-%   \TrinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \TrinaryInfC{<whole sequent or formula>}
-%
-%   \QuaternaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \QuaternaryInfC{<whole sequent or formula>}
-%
-%   \QuinaryInf$<antecendent>\fCenter<succedent>$
-%
-%   \QuinaryInfC{<whole sequent or formula>}
-%
-%   \LeftLabel{<text>} - Puts <text> as a label to the left
-%             of the next inference line.  (Works even if
-%             \noLine is used too.)
-%
-%   \RightLabel{<text>} - Puts <text> as a label to the right of the
-%             next inference line.  (Also works with \noLine.)
-%
-%   \DisplayProof - outputs the whole proof tree (and finishes it).
-%           The proof tree is output as an hbox.
-%
-%
-%   \kernHyps{<dimen>}  - Slides the upper hypotheses right distance <dimen>
-%             (This is similar to shifting conclusion left)
-%           - kernHyps works with Unary, Binary and Trinary
-%             inferences and with centered or uncentered sequents.
-%           - Negative values for <dimen> are permitted.
-%
-%   \insertBetweenHyps{...} - {...} will be inserted between the upper
-%             hypotheses of a Binary or Trinary Inferences.
-%                         It is possible to use negative horizontal space
-%                 to push them closer together (and even overlap).
-%             This command affects only the next inference.
-%
-%   \doubleLine         - Makes the current (ie, next) horizontal line doubled
-%
-%   \alwaysDoubleLine   - Makes lines doubled for rest of proof
-%
-%   \singleLine     - Makes the current (ie, next) line single
-%
-%   \alwaysSingleLine   - Undoes \alwaysDoubleLine or \alwaysNoLine.
-%
-%   \noLine     - Make no line at all at current (ie next) inference.
-%
-%   \alwaysNoLine       - Makes no lines for rest of proof. (Untested)
-%
-%   \solidLine      - Does solid horizontal line for current inference
-%
-%   \dottedLine     - Does dotted horizontal line for current inference
-%
-%   \dashedLine     - Does dashed horizontal line for current inference
-%
-%   \alwaysSolidLine    - Makes the indicated change in line type, permanently
-%   \alwaysDashedLine       until end of proof or until overridden.
-%   \alwaysDottedLine
-%
-%   \bottomAlignProof   - Vertically align proof according to its bottom line.
-%   \centerAlignProof   - Vertically align proof proof precisely in its center.
-%   \normalAlignProof   - Overrides earlier bottom/center AlignProof commands.
-%             The default alignment will look good in most cases,
-%               whether the proof is displayed or is
-%               in-line.  Other alignments may be more
-%               appropriate when putting proofs in tables or
-%               pictures, etc.  For custom alignments, use
-%               TeX's raise commands.
-%
-%   \rootAtTop  - specifies that proofs have their root a the top.  That it,
-%                 proofs will be "upside down".
-%   \rootAtBottom - (default) Specifies that proofs have root at the bottom
-%         The \rootAtTop and \rootAtBottom commands apply *only* to the
-%         current proof.  If you want to make them persistent, use one of
-%         the next two commands:
-%   \alwaysRootAtTop
-%   \alwaysRootAtBottom (default)
-%
-
-% Optional short abbreviations for commands:
-\def\EnableBpAbbreviations{%
-    \let\AX\Axiom
-    \let\AXC\AxiomC
-    \let\UI\UnaryInf
-    \let\UIC\UnaryInfC
-    \let\BI\BinaryInf
-    \let\BIC\BinaryInfC
-    \let\TI\TrinaryInf
-    \let\TIC\TrinaryInfC
-    \let\QI\QuaternaryInf
-    \let\QIC\QuaternaryInfC
-    \let\QuI\QuinaryInf
-    \let\QuIC\QuinaryInfC
-    \let\LL\LeftLabel
-    \let\RL\RightLabel
-    \let\DP\DisplayProof
-}
-
-% Parameters which control the style of the proof trees.
-% The user may wish to override these parameters locally or globally.
-%   BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
-%   future incompatibilities).  Instead, you should change them in your
-%   TeX document right after including this style file in the
-%   header material of your LaTeX document.
-
-\def\ScoreOverhang{4pt}         % How much underlines extend out
-\def\ScoreOverhangLeft{\ScoreOverhang}
-\def\ScoreOverhangRight{\ScoreOverhang}
-
-\def\extraVskip{2pt}            % Extra space above and below lines
-\def\ruleScoreFiller{\hrule}        % Horizontal rule filler.
-\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}}
-\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}
-\def\defaultScoreFiller{\ruleScoreFiller}  % Default horizontal filler.
-\def\defaultBuildScore{\buildSingleScore}  % In \singleLine mode at start.
-
-\def\defaultHypSeparation{\hskip.2in}   % Used if \insertBetweenHyps isn't given
-
-\def\labelSpacing{3pt}      % Horizontal space separating labels and lines
-
-\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex}
-            % Space above and below a prooftree display.
-
-\def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom
-%\def\defaultRootPosition{\buildRootTop}  % Makes all proofs upside down
-
-\ifx\fCenter\undefined
-\def\fCenter{\relax}
-\fi
-
-%
-% End of user-modifiable parameters.
-% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% Here are some internal paramenters and defaults.  Not really intended
-%  to be user-modifiable.
-
-\def\theHypSeparation{\defaultHypSeparation}
-\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler.
-\def\alwaysBuildScore{\defaultBuildScore}
-\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler.
-\def\buildScore{\alwaysBuildScore}   %This command builds the score.
-\def\hypKernAmt{0pt}    % Initial setting for kerning the hypotheses.
-
-\def\defaultLeftLabel{}
-\def\defaultRightLabel{}
-
-\def\myTrue{Y}
-\def\bottomAlignFlag{N}
-\def\centerAlignFlag{N}
-\def\defaultRootAtBottomFlag{Y}
-\def\rootAtBottomFlag{Y}
-
-% End of internal parameters and defaults.
-
-\expandafter\ifx\csname newenvironment\endcsname\relax%
-% If in TeX:
-\message{\BPmessage}
-\def\makeatletter{\catcode`\@=11\relax}
-\def\makeatother{\catcode`\@=12\relax}
-\makeatletter
-\def\newcount{\alloc@0\count\countdef\insc@unt}
-\def\newdimen{\alloc@1\dimen\dimendef\insc@unt}
-\def\newskip{\alloc@2\skip\skipdef\insc@unt}
-\def\newbox{\alloc@4\box\chardef\insc@unt}
-\makeatother
-\else
-% If in LaTeX
-\typeout{\BPmessage}
-\newenvironment{prooftree}%
-{\begin{center}\proofSkipAmount \leavevmode}%
-{\DisplayProof \proofSkipAmount \end{center} }
-\fi
-
-\def\thecur#1{\csname#1\number\theLevel\endcsname}
-
-\newcount\theLevel    % This counter is the height of the stack.
-\global\theLevel=0      % Initialized to zero
-\newcount\myMaxLevel
-\global\myMaxLevel=0
-\newbox\myBoxA      % Temporary storage boxes
-\newbox\myBoxB
-\newbox\myBoxC
-\newbox\myBoxD
-\newbox\myBoxLL     % Boxes for the left label and the right label.
-\newbox\myBoxRL
-\newdimen\thisAboveSkip     %Internal use: amount to skip above line
-\newdimen\thisBelowSkip     %Internal use: amount to skip below line
-\newdimen\newScoreStart     % More temporary storage.
-\newdimen\newScoreEnd
-\newdimen\newCenter
-\newdimen\displace
-\newdimen\leftLowerAmt%     Amount to lower left label
-\newdimen\rightLowerAmt%    Amount to lower right label
-\newdimen\scoreHeight%      Score height
-\newdimen\scoreDepth%       Score Depth
-\newdimen\htLbox%
-\newdimen\htRbox%
-\newdimen\htRRbox%
-\newdimen\htRRRbox%
-\newdimen\htAbox%
-\newdimen\htCbox%
-
-\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
-\setbox\myBoxRL=\hbox{\defaultRightLabel}%
-
-\def\allocatemore{%
-    \ifnum\theLevel>\myMaxLevel%
-        \expandafter\newbox\curBox%
-        \expandafter\newdimen\curScoreStart%
-        \expandafter\newdimen\curCenter%
-        \expandafter\newdimen\curScoreEnd%
-        \global\advance\myMaxLevel by1%
-    \fi%
-}
-
-\def\prepAxiom{%
-    \advance\theLevel by1%
-    \edef\curBox{\thecur{myBox}}%
-    \edef\curScoreStart{\thecur{myScoreStart}}%
-    \edef\curCenter{\thecur{myCenter}}%
-    \edef\curScoreEnd{\thecur{myScoreEnd}}%
-    \allocatemore%
-}
-
-\def\Axiom$#1\fCenter#2${%
-    % Get level and correct names set.
-    \prepAxiom%
-    % Define the boxes
-    \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
-    \setbox\myBoxB=\hbox{$#2$}%
-    \global\setbox\curBox=%
-         \hbox{\hskip\ScoreOverhangLeft\relax%
-        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
-    % Set the relevant dimensions for the boxes
-    \global\curScoreStart=0pt \relax
-    \global\curScoreEnd=\wd\curBox \relax
-    \global\curCenter=\wd\myBoxA \relax
-    \global\advance \curCenter by \ScoreOverhangLeft%
-    \ignorespaces
-}
-
-\def\AxiomC#1{      % Note argument not in math mode
-    % Get level and correct names set.
-    \prepAxiom%
-        % Define the box.
-    \setbox\myBoxA=\hbox{#1}%
-    \global\setbox\curBox =%
-        \hbox{\hskip\ScoreOverhangLeft\relax%
-                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
-    % Set the relevant dimensions for the boxes
-        \global\curScoreStart=0pt \relax
-        \global\curScoreEnd=\wd\curBox \relax
-        \global\curCenter=.5\wd\curBox \relax
-        \global\advance \curCenter by \ScoreOverhangLeft%
-    \ignorespaces
-}
-
-\def\prepUnary{%
-    \ifnum \theLevel<1
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\curBox{\thecur{myBox}}%
-    \edef\curScoreStart{\thecur{myScoreStart}}%
-    \edef\curCenter{\thecur{myCenter}}%
-    \edef\curScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\UnaryInf$#1\fCenter#2${%
-    \prepUnary%
-    \buildConclusion{#1}{#2}%
-    \joinUnary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\UnaryInfC#1{
-    \prepUnary%
-    \buildConclusionC{#1}%
-    %Align and join the curBox and the new box into one vbox.
-    \joinUnary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\prepBinary{%
-    \ifnum\theLevel<2
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\BinaryInf$#1\fCenter#2${%
-    \prepBinary%
-    \buildConclusion{#1}{#2}%
-    \joinBinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\BinaryInfC#1{%
-    \prepBinary%
-    \buildConclusionC{#1}%
-    \joinBinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\prepTrinary{%
-    \ifnum\theLevel<3
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\TrinaryInf$#1\fCenter#2${%
-    \prepTrinary%
-    \buildConclusion{#1}{#2}%
-    \joinTrinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\TrinaryInfC#1{%
-    \prepTrinary%
-    \buildConclusionC{#1}%
-    \joinTrinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\def\prepQuaternary{%
-    \ifnum\theLevel<4
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rrcurBox{\thecur{myBox}}%   Set up names of very right hypothesis
-    \edef\rrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrcurCenter{\thecur{myCenter}}%
-    \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\QuaternaryInf$#1\fCenter#2${%
-    \prepQuaternary%
-    \buildConclusion{#1}{#2}%
-    \joinQuaternary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\QuaternaryInfC#1{%
-    \prepQuaternary%
-    \buildConclusionC{#1}%
-    \joinQuaternary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\joinQuaternary{% Construct the quarterary inference into a vbox.
-    % Join the four hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rrcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\rcurBox%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by3\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox
-                      \unhcopy\myBoxA\box\rrcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \htRRbox = \ht\rrcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\def\prepQuinary{%
-    \ifnum\theLevel<5
-        \errmessage{Hypotheses missing!}
-    \fi%
-    \edef\rrrcurBox{\thecur{myBox}}%   Set up names of very very right hypothesis
-    \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrrcurCenter{\thecur{myCenter}}%
-    \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rrcurBox{\thecur{myBox}}%   Set up names of very right hypothesis
-    \edef\rrcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rrcurCenter{\thecur{myCenter}}%
-    \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\rcurBox{\thecur{myBox}}%   Set up names of right hypothesis
-    \edef\rcurScoreStart{\thecur{myScoreStart}}%
-    \edef\rcurCenter{\thecur{myCenter}}%
-    \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
-    \edef\ccurScoreStart{\thecur{myScoreStart}}%
-    \edef\ccurCenter{\thecur{myCenter}}%
-    \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
-    \advance\theLevel by-1%
-    \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
-    \edef\lcurScoreStart{\thecur{myScoreStart}}%
-    \edef\lcurCenter{\thecur{myCenter}}%
-    \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
-}
-
-\def\QuinaryInf$#1\fCenter#2${%
-    \prepQuinary%
-    \buildConclusion{#1}{#2}%
-    \joinQuinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\QuinaryInfC#1{%
-    \prepQuinary%
-    \buildConclusionC{#1}%
-    \joinQuinary%
-    \resetInferenceDefaults%
-    \ignorespaces%
-}
-
-\def\joinQuinary{% Construct the quinary inference into a vbox.
-    % Join the five hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rrrcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\rrcurBox%
-    \advance\lcurScoreEnd by\wd\rcurBox%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by4\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox
-                      \unhcopy\myBoxA\box\rrcurBox
-                      \unhcopy\myBoxA\box\rrrcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \htRRbox = \ht\rrcurBox%
-        \htRRRbox = \ht\rrrcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
-    % Define the boxes
-        \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
-        \setbox\myBoxB=\hbox{$#2$}%
-    % Put them together in \myBoxC
-    \setbox\myBoxC =%
-          \hbox{\hskip\ScoreOverhangLeft\relax%
-        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
-    % Calculate the center of the \myBoxC string.
-    \newScoreStart=0pt \relax%
-    \newCenter=\wd\myBoxA \relax%
-    \advance \newCenter by \ScoreOverhangLeft%
-    \newScoreEnd=\wd\myBoxC%
-}
-
-\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
-        % Define the box.
-    \setbox\myBoxA=\hbox{#1}%
-    \setbox\myBoxC =%
-        \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
-                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
-    % Calculate kerning to line up centers
-    \newScoreStart=0pt \relax%
-    \newCenter=.5\wd\myBoxC \relax%
-    \newScoreEnd=\wd\myBoxC%
-        \advance \newCenter by \ScoreOverhangLeft%
-}
-
-\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox
-    \global\advance\curCenter by -\hypKernAmt%
-    \ifnum\curCenter<\newCenter%
-        \displace=\newCenter%
-        \advance \displace by -\curCenter%
-        \kernUpperBox%
-    \else%
-        \displace=\curCenter%
-        \advance \displace by -\newCenter%
-        \kernLowerBox%
-    \fi%
-        \ifnum \newScoreStart < \curScoreStart %
-        \global \curScoreStart = \newScoreStart \fi%
-    \ifnum \curScoreEnd < \newScoreEnd %
-        \global \curScoreEnd = \newScoreEnd \fi%
-    % Leave room for the left label.
-    \ifnum \curScoreStart<\wd\myBoxLL%
-        \global\displace = \wd\myBoxLL%
-        \global\advance\displace by -\curScoreStart%
-        \kernUpperBox%
-        \kernLowerBox%
-    \fi%
-    % Draw the score
-    \buildScore%
-    % Form the score and labels into a box.
-    \buildScoreLabels%
-    % Form the new box and its dimensions
-    \ifx\rootAtBottomFlag\myTrue%
-        \buildRootBottom%
-    \else%
-        \buildRootTop%
-    \fi%
-    \global \curScoreStart=\newScoreStart%
-    \global \curScoreEnd=\newScoreEnd%
-    \global \curCenter=\newCenter%
-}
-
-\def\buildRootBottom{%
-    \global \setbox \curBox =%
-        \vbox{\box\curBox%
-            \vskip\thisAboveSkip \relax%
-            \nointerlineskip\box\myBoxD%
-            \vskip\thisBelowSkip \relax%
-            \nointerlineskip\box\myBoxC}%
-}
-
-\def\buildRootTop{%
-    \global \setbox \curBox =%
-        \vbox{\box\myBoxC%
-            \vskip\thisAboveSkip \relax%
-            \nointerlineskip\box\myBoxD%
-            \vskip\thisBelowSkip \relax%
-            \nointerlineskip\box\curBox}%
-}
-
-\def\kernUpperBox{%
-        \global\setbox\curBox =%
-            \hbox{\hskip\displace\box\curBox}%
-        \global\advance \curScoreStart by \displace%
-        \global\advance \curScoreEnd by \displace%
-        \global\advance\curCenter by \displace%
-}
-
-\def\kernLowerBox{%
-        \global\setbox\myBoxC =%
-            \hbox{\hskip\displace\unhbox\myBoxC}%
-        \global\advance \newScoreStart by \displace%
-        \global\advance \newScoreEnd by \displace%
-        \global\advance\newCenter by \displace%
-}
-
-\def\joinBinary{% Construct the binary inference into a vbox.
-    % Join the two hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htRbox = \ht\rcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-\def\joinTrinary{% Construct the trinary inference into a vbox.
-    % Join the three hypotheses's boxes into one hbox.
-    \setbox\myBoxA=\hbox{\theHypSeparation}%
-    \lcurScoreEnd=\rcurScoreEnd%
-    \advance\lcurScoreEnd by\wd\lcurBox%
-    \advance\lcurScoreEnd by\wd\ccurBox%
-    \advance\lcurScoreEnd by2\wd\myBoxA%
-    \displace=\lcurScoreEnd%
-    \advance\displace by -\lcurScoreStart%
-    \lcurCenter=.5\displace%
-    \advance\lcurCenter by\lcurScoreStart%
-    \ifx\rootAtBottomFlag\myTrue%
-        \setbox\lcurBox=%
-            \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
-                      \unhcopy\myBoxA\box\rcurBox}%
-    \else%
-        \htLbox = \ht\lcurBox%
-        \htAbox = \ht\myBoxA%
-        \htCbox = \ht\ccurBox%
-        \htRbox = \ht\rcurBox%
-        \setbox\lcurBox=%
-            \hbox{\lower\htLbox\box\lcurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
-                  \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
-    \fi%
-    % Adjust center of upper hypotheses according to how much
-    %   the lower sequent is off-center.
-    \displace=\newCenter%
-    \advance\displace by -.5\newScoreStart%
-    \advance\displace by -.5\newScoreEnd%
-    \advance\lcurCenter by \displace%
-    %Align and join the curBox and the two hypotheses's box into one vbox.
-    \edef\curBox{\lcurBox}%
-    \edef\curScoreStart{\lcurScoreStart}%
-    \edef\curScoreEnd{\lcurScoreEnd}%
-    \edef\curCenter{\lcurCenter}%
-    \joinUnary%
-}
-
-\def\DisplayProof{%
-    % Display (and purge) the proof tree.
-    % Choose the appropriate vertical alignment.
-    \ifnum \theLevel=1 \relax \else%x
-        \errmessage{Proof tree badly specified.}%
-    \fi%
-    \edef\curBox{\thecur{myBox}}%
-    \ifx\bottomAlignFlag\myTrue%
-        \displace=0pt%
-    \else%
-        \displace=.5\ht\curBox%
-        \ifx\centerAlignFlag\myTrue\relax
-        \else%
-                \advance\displace by -3pt%
-        \fi%
-    \fi%
-    \leavevmode%
-    \lower\displace\hbox{\copy\curBox}%
-    \global\theLevel=0%
-    \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always"
-    \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always"
-    \global\def\bottomAlignFlag{N}%
-    \global\def\centerAlignFlag{N}%
-    \resetRootPosition
-    \resetInferenceDefaults%
-    \ignorespaces
-}
-
-\def\buildSingleScore{% Make an hbox with a single score.
-    \displace=\curScoreEnd%
-    \advance \displace by -\curScoreStart%
-    \global\setbox \myBoxD =%
-        \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}%
-    %\global\setbox \myBoxD =%
-        %\hbox{\hskip\curScoreStart\relax \box\myBoxD}%
-}
-
-\def\buildDoubleScore{% Make an hbox with a double score.
-    \buildSingleScore%
-    \global\setbox\myBoxD=%
-        \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}%
-}
-
-\def\buildNoScore{% Make an hbox with no score (raise a little anyway)
-    \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}%
-}
-
-\def\doubleLine{%
-    \gdef\buildScore{\buildDoubleScore}% Set next score to this type
-    \ignorespaces
-}
-\def\alwaysDoubleLine{%
-    \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof.
-    \gdef\buildScore{\buildDoubleScore}% Set next score to be double
-    \ignorespaces
-}
-\def\singleLine{%
-    \gdef\buildScore{\buildSingleScore}% Set next score to be single
-    \ignorespaces
-}
-\def\alwaysSingleLine{%
-    \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof.
-    \gdef\buildScore{\buildSingleScore}% Set next score to be single
-    \ignorespaces
-}
-\def\noLine{%
-    \gdef\buildScore{\buildNoScore}% Set next score to this type
-    \ignorespaces
-}
-\def\alwaysNoLine{%
-    \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof.
-    \gdef\buildScore{\buildNoScore}% Set next score to be blank
-    \ignorespaces
-}
-\def\solidLine{%
-    \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
-    \ignorespaces
-}
-\def\alwaysSolidLine{%
-    \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof
-    \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
-    \ignorespaces
-}
-\def\dottedLine{%
-    \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
-    \ignorespaces
-}
-\def\alwaysDottedLine{%
-    \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof
-    \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
-    \ignorespaces
-}
-\def\dashedLine{%
-    \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
-    \ignorespaces
-}
-\def\alwaysDashedLine{%
-    \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof
-    \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
-    \ignorespaces
-}
-\def\kernHyps#1{%
-    \gdef\hypKernAmt{#1}%
-    \ignorespaces
-}
-\def\insertBetweenHyps#1{%
-    \gdef\theHypSeparation{#1}%
-    \ignorespaces
-}
-
-\def\centerAlignProof{%
-    \def\centerAlignFlag{Y}%
-    \def\bottomAlignFlag{N}%
-    \ignorespaces
-}
-\def\bottomAlignProof{%
-    \def\centerAlignFlag{N}%
-    \def\bottomAlignFlag{Y}%
-    \ignorespaces
-}
-\def\normalAlignProof{%
-    \def\centerAlignFlag{N}%
-    \def\bottomAlignFlag{N}%
-    \ignorespaces
-}
-
-\def\LeftLabel#1{%
-    \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}%
-    \ignorespaces
-}
-\def\RightLabel#1{%
-    \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}%
-    \ignorespaces
-}
-
-\def\buildScoreLabels{%
-    \scoreHeight = \ht\myBoxD%
-    \scoreDepth = \dp\myBoxD%
-    \leftLowerAmt=\ht\myBoxLL%
-    \advance \leftLowerAmt by -\dp\myBoxLL%
-    \advance \leftLowerAmt by -\scoreHeight%
-    \advance \leftLowerAmt by \scoreDepth%
-    \leftLowerAmt=.5\leftLowerAmt%
-    \rightLowerAmt=\ht\myBoxRL%
-    \advance \rightLowerAmt by -\dp\myBoxRL%
-    \advance \rightLowerAmt by -\scoreHeight%
-    \advance \rightLowerAmt by \scoreDepth%
-    \rightLowerAmt=.5\rightLowerAmt%
-    \displace = \curScoreStart%
-    \advance\displace by -\wd\myBoxLL%
-    \global\setbox\myBoxD =%
-        \hbox{\hskip\displace%
-            \lower\leftLowerAmt\copy\myBoxLL%
-            \box\myBoxD%
-            \lower\rightLowerAmt\copy\myBoxRL}%
-    \global\thisAboveSkip = \ht\myBoxLL%
-    \global\advance \thisAboveSkip by -\leftLowerAmt%
-    \global\advance \thisAboveSkip by -\scoreHeight%
-    \ifnum \thisAboveSkip<0 %
-        \global\thisAboveSkip=0pt%
-    \fi%
-    \displace = \ht\myBoxRL%
-    \advance \displace by -\rightLowerAmt%
-    \advance \displace by -\scoreHeight%
-    \ifnum \displace<0 %
-        \displace=0pt%
-    \fi%
-    \ifnum \displace>\thisAboveSkip %
-        \global\thisAboveSkip=\displace%
-    \fi%
-    \global\thisBelowSkip = \dp\myBoxLL%
-    \global\advance\thisBelowSkip by \leftLowerAmt%
-    \global\advance\thisBelowSkip by -\scoreDepth%
-    \ifnum\thisBelowSkip<0 %
-        \global\thisBelowSkip = 0pt%
-    \fi%
-    \displace = \dp\myBoxRL%
-    \advance\displace by \rightLowerAmt%
-    \advance\displace by -\scoreDepth%
-    \ifnum\displace<0 %
-        \displace = 0pt%
-    \fi%
-    \ifnum\displace>\thisBelowSkip%
-        \global\thisBelowSkip = \displace%
-    \fi%
-    \global\thisAboveSkip = -\thisAboveSkip%
-    \global\thisBelowSkip = -\thisBelowSkip%
-    \global\advance\thisAboveSkip by\extraVskip% Extra space above line
-    \global\advance\thisBelowSkip by\extraVskip% Extra space below line
-}
-
-\def\resetInferenceDefaults{%
-    \global\def\theHypSeparation{\defaultHypSeparation}%
-    \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
-    \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
-    \global\def\buildScore{\alwaysBuildScore}%
-    \global\def\theScoreFiller{\alwaysScoreFiller}%
-    \gdef\hypKernAmt{0pt}% Restore to zero kerning.
-}
-
-
-\def\rootAtBottom{%
-    \global\def\rootAtBottomFlag{Y}%
-}
-
-\def\rootAtTop{%
-    \global\def\rootAtBottomFlag{N}%
-}
-
-\def\resetRootPosition{%
-    \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag}
-}
-
-\def\alwaysRootAtBottom{%
-    \global\def\defaultRootAtBottomFlag{Y}
-    \rootAtBottom
-}
-
-\def\alwaysRootAtTop{%
-    \global\def\defaultRootAtBottomFlag{N}
-    \rootAtTop
-}
-
-

Binary file final_pre/modus-ponens/modus-ponens.pdf has changed

--- a/final_pre/modus-ponens/modus-ponens.svg	Tue Feb 19 14:14:30 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="595.28pt" height="841.89pt" viewBox="0 0 595.28 841.89" version="1.1">
-<defs>
-<g>
-<symbol overflow="visible" id="glyph0-0">
-<path style="stroke:none;" d=""/>
-</symbol>
-<symbol overflow="visible" id="glyph0-1">
-<path style="stroke:none;" d="M 2.546875 2.5 L 2.546875 2.09375 L 1.578125 2.09375 L 1.578125 -7.078125 L 2.546875 -7.078125 L 2.546875 -7.484375 L 1.171875 -7.484375 L 1.171875 2.5 Z M 2.546875 2.5 "/>
-</symbol>
-<symbol overflow="visible" id="glyph0-2">
-<path style="stroke:none;" d="M 1.578125 -7.484375 L 0.21875 -7.484375 L 0.21875 -7.078125 L 1.1875 -7.078125 L 1.1875 2.09375 L 0.21875 2.09375 L 0.21875 2.5 L 1.578125 2.5 Z M 1.578125 -7.484375 "/>
-</symbol>
-<symbol overflow="visible" id="glyph0-3">
-<path style="stroke:none;" d="M 3.296875 2.390625 C 3.296875 2.359375 3.296875 2.34375 3.125 2.171875 C 1.890625 0.921875 1.5625 -0.96875 1.5625 -2.5 C 1.5625 -4.234375 1.9375 -5.96875 3.171875 -7.203125 C 3.296875 -7.328125 3.296875 -7.34375 3.296875 -7.375 C 3.296875 -7.453125 3.265625 -7.484375 3.203125 -7.484375 C 3.09375 -7.484375 2.203125 -6.796875 1.609375 -5.53125 C 1.109375 -4.4375 0.984375 -3.328125 0.984375 -2.5 C 0.984375 -1.71875 1.09375 -0.515625 1.640625 0.625 C 2.25 1.84375 3.09375 2.5 3.203125 2.5 C 3.265625 2.5 3.296875 2.46875 3.296875 2.390625 Z M 3.296875 2.390625 "/>
-</symbol>
-<symbol overflow="visible" id="glyph0-4">
-<path style="stroke:none;" d="M 2.875 -2.5 C 2.875 -3.265625 2.765625 -4.46875 2.21875 -5.609375 C 1.625 -6.828125 0.765625 -7.484375 0.671875 -7.484375 C 0.609375 -7.484375 0.5625 -7.4375 0.5625 -7.375 C 0.5625 -7.34375 0.5625 -7.328125 0.75 -7.140625 C 1.734375 -6.15625 2.296875 -4.578125 2.296875 -2.5 C 2.296875 -0.78125 1.9375 0.96875 0.703125 2.21875 C 0.5625 2.34375 0.5625 2.359375 0.5625 2.390625 C 0.5625 2.453125 0.609375 2.5 0.671875 2.5 C 0.765625 2.5 1.671875 1.8125 2.25 0.546875 C 2.765625 -0.546875 2.875 -1.65625 2.875 -2.5 Z M 2.875 -2.5 "/>
-</symbol>
-<symbol overflow="visible" id="glyph0-5">
-<path style="stroke:none;" d="M 2.9375 -6.375 C 2.9375 -6.625 2.9375 -6.640625 2.703125 -6.640625 C 2.078125 -6 1.203125 -6 0.890625 -6 L 0.890625 -5.6875 C 1.09375 -5.6875 1.671875 -5.6875 2.1875 -5.953125 L 2.1875 -0.78125 C 2.1875 -0.421875 2.15625 -0.3125 1.265625 -0.3125 L 0.953125 -0.3125 L 0.953125 0 C 1.296875 -0.03125 2.15625 -0.03125 2.5625 -0.03125 C 2.953125 -0.03125 3.828125 -0.03125 4.171875 0 L 4.171875 -0.3125 L 3.859375 -0.3125 C 2.953125 -0.3125 2.9375 -0.421875 2.9375 -0.78125 Z M 2.9375 -6.375 "/>
-</symbol>
-<symbol overflow="visible" id="glyph0-6">
-<path style="stroke:none;" d="M 1.265625 -0.765625 L 2.328125 -1.796875 C 3.875 -3.171875 4.46875 -3.703125 4.46875 -4.703125 C 4.46875 -5.84375 3.578125 -6.640625 2.359375 -6.640625 C 1.234375 -6.640625 0.5 -5.71875 0.5 -4.828125 C 0.5 -4.28125 1 -4.28125 1.03125 -4.28125 C 1.203125 -4.28125 1.546875 -4.390625 1.546875 -4.8125 C 1.546875 -5.0625 1.359375 -5.328125 1.015625 -5.328125 C 0.9375 -5.328125 0.921875 -5.328125 0.890625 -5.3125 C 1.109375 -5.96875 1.65625 -6.328125 2.234375 -6.328125 C 3.140625 -6.328125 3.5625 -5.515625 3.5625 -4.703125 C 3.5625 -3.90625 3.078125 -3.125 2.515625 -2.5 L 0.609375 -0.375 C 0.5 -0.265625 0.5 -0.234375 0.5 0 L 4.203125 0 L 4.46875 -1.734375 L 4.234375 -1.734375 C 4.171875 -1.4375 4.109375 -1 4 -0.84375 C 3.9375 -0.765625 3.28125 -0.765625 3.0625 -0.765625 Z M 1.265625 -0.765625 "/>
-</symbol>
-<symbol overflow="visible" id="glyph1-0">
-<path style="stroke:none;" d=""/>
-</symbol>
-<symbol overflow="visible" id="glyph1-1">
-<path style="stroke:none;" d="M 1.78125 -1.140625 C 1.390625 -0.484375 1 -0.34375 0.5625 -0.3125 C 0.4375 -0.296875 0.34375 -0.296875 0.34375 -0.109375 C 0.34375 -0.046875 0.40625 0 0.484375 0 C 0.75 0 1.0625 -0.03125 1.328125 -0.03125 C 1.671875 -0.03125 2.015625 0 2.328125 0 C 2.390625 0 2.515625 0 2.515625 -0.1875 C 2.515625 -0.296875 2.4375 -0.3125 2.359375 -0.3125 C 2.140625 -0.328125 1.890625 -0.40625 1.890625 -0.65625 C 1.890625 -0.78125 1.953125 -0.890625 2.03125 -1.03125 L 2.796875 -2.296875 L 5.296875 -2.296875 C 5.3125 -2.09375 5.453125 -0.734375 5.453125 -0.640625 C 5.453125 -0.34375 4.9375 -0.3125 4.734375 -0.3125 C 4.59375 -0.3125 4.5 -0.3125 4.5 -0.109375 C 4.5 0 4.609375 0 4.640625 0 C 5.046875 0 5.46875 -0.03125 5.875 -0.03125 C 6.125 -0.03125 6.765625 0 7.015625 0 C 7.0625 0 7.1875 0 7.1875 -0.203125 C 7.1875 -0.3125 7.09375 -0.3125 6.953125 -0.3125 C 6.34375 -0.3125 6.34375 -0.375 6.3125 -0.671875 L 5.703125 -6.890625 C 5.6875 -7.09375 5.6875 -7.140625 5.515625 -7.140625 C 5.359375 -7.140625 5.3125 -7.0625 5.25 -6.96875 Z M 2.984375 -2.609375 L 4.9375 -5.90625 L 5.265625 -2.609375 Z M 2.984375 -2.609375 "/>
-</symbol>
-<symbol overflow="visible" id="glyph1-2">
-<path style="stroke:none;" d="M 1.59375 -0.78125 C 1.5 -0.390625 1.46875 -0.3125 0.6875 -0.3125 C 0.515625 -0.3125 0.421875 -0.3125 0.421875 -0.109375 C 0.421875 0 0.515625 0 0.6875 0 L 4.25 0 C 5.828125 0 7 -1.171875 7 -2.15625 C 7 -2.875 6.421875 -3.453125 5.453125 -3.5625 C 6.484375 -3.75 7.53125 -4.484375 7.53125 -5.4375 C 7.53125 -6.171875 6.875 -6.8125 5.6875 -6.8125 L 2.328125 -6.8125 C 2.140625 -6.8125 2.046875 -6.8125 2.046875 -6.609375 C 2.046875 -6.5 2.140625 -6.5 2.328125 -6.5 C 2.34375 -6.5 2.53125 -6.5 2.703125 -6.484375 C 2.875 -6.453125 2.96875 -6.453125 2.96875 -6.3125 C 2.96875 -6.28125 2.953125 -6.25 2.9375 -6.125 Z M 3.09375 -3.65625 L 3.71875 -6.125 C 3.8125 -6.46875 3.828125 -6.5 4.25 -6.5 L 5.546875 -6.5 C 6.421875 -6.5 6.625 -5.90625 6.625 -5.46875 C 6.625 -4.59375 5.765625 -3.65625 4.5625 -3.65625 Z M 2.65625 -0.3125 C 2.515625 -0.3125 2.5 -0.3125 2.4375 -0.3125 C 2.328125 -0.328125 2.296875 -0.34375 2.296875 -0.421875 C 2.296875 -0.453125 2.296875 -0.46875 2.359375 -0.640625 L 3.046875 -3.421875 L 4.921875 -3.421875 C 5.875 -3.421875 6.078125 -2.6875 6.078125 -2.265625 C 6.078125 -1.28125 5.1875 -0.3125 4 -0.3125 Z M 2.65625 -0.3125 "/>
-</symbol>
-<symbol overflow="visible" id="glyph1-3">
-<path style="stroke:none;" d="M 7.578125 -6.921875 C 7.578125 -6.953125 7.5625 -7.03125 7.46875 -7.03125 C 7.4375 -7.03125 7.421875 -7.015625 7.3125 -6.90625 L 6.625 -6.140625 C 6.53125 -6.28125 6.078125 -7.03125 4.96875 -7.03125 C 2.734375 -7.03125 0.5 -4.828125 0.5 -2.515625 C 0.5 -0.875 1.671875 0.21875 3.203125 0.21875 C 4.0625 0.21875 4.828125 -0.171875 5.359375 -0.640625 C 6.28125 -1.453125 6.453125 -2.359375 6.453125 -2.390625 C 6.453125 -2.5 6.34375 -2.5 6.328125 -2.5 C 6.265625 -2.5 6.21875 -2.46875 6.203125 -2.390625 C 6.109375 -2.109375 5.875 -1.390625 5.1875 -0.8125 C 4.5 -0.265625 3.875 -0.09375 3.359375 -0.09375 C 2.46875 -0.09375 1.40625 -0.609375 1.40625 -2.15625 C 1.40625 -2.734375 1.609375 -4.34375 2.609375 -5.515625 C 3.21875 -6.21875 4.15625 -6.71875 5.046875 -6.71875 C 6.0625 -6.71875 6.65625 -5.953125 6.65625 -4.796875 C 6.65625 -4.390625 6.625 -4.390625 6.625 -4.28125 C 6.625 -4.1875 6.734375 -4.1875 6.765625 -4.1875 C 6.890625 -4.1875 6.890625 -4.203125 6.953125 -4.390625 Z M 7.578125 -6.921875 "/>
-</symbol>
-<symbol overflow="visible" id="glyph2-0">
-<path style="stroke:none;" d=""/>
-</symbol>
-<symbol overflow="visible" id="glyph2-1">
-<path style="stroke:none;" d="M 2.46875 -5.21875 C 1.15625 -4.296875 0.796875 -2.8125 0.796875 -1.75 C 0.796875 -0.765625 1.09375 0.765625 2.46875 1.734375 C 2.53125 1.734375 2.609375 1.734375 2.609375 1.65625 C 2.609375 1.609375 2.59375 1.59375 2.546875 1.546875 C 1.609375 0.703125 1.28125 -0.46875 1.28125 -1.734375 C 1.28125 -3.625 2 -4.546875 2.5625 -5.0625 C 2.59375 -5.09375 2.609375 -5.109375 2.609375 -5.140625 C 2.609375 -5.21875 2.53125 -5.21875 2.46875 -5.21875 Z M 2.46875 -5.21875 "/>
-</symbol>
-<symbol overflow="visible" id="glyph2-2">
-<path style="stroke:none;" d="M 2.328125 -4.4375 C 2.328125 -4.625 2.328125 -4.625 2.125 -4.625 C 1.671875 -4.1875 1.046875 -4.1875 0.765625 -4.1875 L 0.765625 -3.9375 C 0.921875 -3.9375 1.390625 -3.9375 1.765625 -4.125 L 1.765625 -0.578125 C 1.765625 -0.34375 1.765625 -0.25 1.078125 -0.25 L 0.8125 -0.25 L 0.8125 0 C 0.9375 0 1.796875 -0.03125 2.046875 -0.03125 C 2.265625 -0.03125 3.140625 0 3.296875 0 L 3.296875 -0.25 L 3.03125 -0.25 C 2.328125 -0.25 2.328125 -0.34375 2.328125 -0.578125 Z M 2.328125 -4.4375 "/>
-</symbol>
-<symbol overflow="visible" id="glyph2-3">
-<path style="stroke:none;" d="M 0.625 -5.21875 C 0.578125 -5.21875 0.5 -5.21875 0.5 -5.140625 C 0.5 -5.109375 0.515625 -5.09375 0.5625 -5.03125 C 1.15625 -4.484375 1.828125 -3.546875 1.828125 -1.75 C 1.828125 -0.296875 1.375 0.8125 0.625 1.484375 C 0.5 1.609375 0.5 1.609375 0.5 1.65625 C 0.5 1.6875 0.515625 1.734375 0.578125 1.734375 C 0.671875 1.734375 1.328125 1.28125 1.796875 0.40625 C 2.09375 -0.171875 2.296875 -0.921875 2.296875 -1.734375 C 2.296875 -2.71875 2 -4.25 0.625 -5.21875 Z M 0.625 -5.21875 "/>
-</symbol>
-<symbol overflow="visible" id="glyph2-4">
-<path style="stroke:none;" d="M 3.515625 -1.265625 L 3.28125 -1.265625 C 3.265625 -1.109375 3.1875 -0.703125 3.09375 -0.640625 C 3.046875 -0.59375 2.515625 -0.59375 2.40625 -0.59375 L 1.125 -0.59375 C 1.859375 -1.234375 2.109375 -1.4375 2.515625 -1.765625 C 3.03125 -2.171875 3.515625 -2.609375 3.515625 -3.265625 C 3.515625 -4.109375 2.78125 -4.625 1.890625 -4.625 C 1.03125 -4.625 0.4375 -4.015625 0.4375 -3.375 C 0.4375 -3.03125 0.734375 -2.984375 0.8125 -2.984375 C 0.96875 -2.984375 1.171875 -3.109375 1.171875 -3.359375 C 1.171875 -3.484375 1.125 -3.734375 0.765625 -3.734375 C 0.984375 -4.21875 1.453125 -4.375 1.78125 -4.375 C 2.484375 -4.375 2.84375 -3.828125 2.84375 -3.265625 C 2.84375 -2.65625 2.40625 -2.1875 2.1875 -1.9375 L 0.515625 -0.265625 C 0.4375 -0.203125 0.4375 -0.1875 0.4375 0 L 3.3125 0 Z M 3.515625 -1.265625 "/>
-</symbol>
-<symbol overflow="visible" id="glyph3-0">
-<path style="stroke:none;" d=""/>
-</symbol>
-<symbol overflow="visible" id="glyph3-1">
-<path style="stroke:none;" d="M 7.234375 -3.265625 C 7.65625 -2.90625 8.171875 -2.640625 8.5 -2.5 C 8.140625 -2.328125 7.640625 -2.078125 7.234375 -1.71875 L 0.90625 -1.71875 C 0.734375 -1.71875 0.546875 -1.71875 0.546875 -1.53125 C 0.546875 -1.328125 0.734375 -1.328125 0.890625 -1.328125 L 6.78125 -1.328125 C 6.3125 -0.875 5.796875 0.015625 5.796875 0.140625 C 5.796875 0.25 5.921875 0.25 5.984375 0.25 C 6.0625 0.25 6.125 0.25 6.171875 0.171875 C 6.375 -0.203125 6.65625 -0.734375 7.3125 -1.3125 C 8 -1.921875 8.65625 -2.1875 9.1875 -2.34375 C 9.34375 -2.40625 9.359375 -2.40625 9.375 -2.4375 C 9.40625 -2.4375 9.40625 -2.46875 9.40625 -2.5 C 9.40625 -2.515625 9.40625 -2.53125 9.390625 -2.546875 L 9.359375 -2.578125 C 9.34375 -2.578125 9.328125 -2.59375 9.140625 -2.65625 C 7.796875 -3.046875 6.796875 -3.953125 6.234375 -5.03125 C 6.125 -5.21875 6.125 -5.234375 5.984375 -5.234375 C 5.921875 -5.234375 5.796875 -5.234375 5.796875 -5.125 C 5.796875 -5 6.296875 -4.125 6.78125 -3.65625 L 0.890625 -3.65625 C 0.734375 -3.65625 0.546875 -3.65625 0.546875 -3.453125 C 0.546875 -3.265625 0.734375 -3.265625 0.90625 -3.265625 Z M 7.234375 -3.265625 "/>
-</symbol>
-<symbol overflow="visible" id="glyph3-2">
-<path style="stroke:none;" d="M 3.546875 -5.75 C 3.46875 -5.921875 3.40625 -5.96875 3.3125 -5.96875 C 3.1875 -5.96875 3.15625 -5.890625 3.09375 -5.75 L 0.625 -0.171875 C 0.5625 -0.046875 0.546875 -0.03125 0.546875 0.015625 C 0.546875 0.125 0.640625 0.21875 0.75 0.21875 C 0.8125 0.21875 0.890625 0.203125 0.984375 0.015625 L 3.3125 -5.28125 L 5.65625 0.015625 C 5.75 0.21875 5.859375 0.21875 5.890625 0.21875 C 6 0.21875 6.09375 0.125 6.09375 0.015625 C 6.09375 0 6.09375 -0.015625 6.03125 -0.140625 Z M 3.546875 -5.75 "/>
-</symbol>
-<symbol overflow="visible" id="glyph3-3">
-<path style="stroke:none;" d="M 2.375 -3.625 C 0.390625 -2.546875 0.28125 -1.25 0.28125 -1.015625 C 0.28125 -0.265625 1.015625 0.21875 1.96875 0.21875 C 3.625 0.21875 4.96875 -1.359375 4.96875 -1.5625 C 4.96875 -1.625 4.921875 -1.640625 4.859375 -1.640625 C 4.75 -1.640625 4.359375 -1.5 4.140625 -1.203125 C 3.921875 -0.90625 3.515625 -0.328125 2.625 -0.328125 C 1.90625 -0.328125 1.125 -0.703125 1.125 -1.453125 C 1.125 -1.9375 1.6875 -3.40625 3.265625 -3.46875 C 3.734375 -3.484375 4.078125 -3.84375 4.078125 -3.953125 C 4.078125 -4 4.03125 -4.015625 3.984375 -4.015625 C 2.578125 -4.078125 2.296875 -4.765625 2.296875 -5.15625 C 2.296875 -5.390625 2.4375 -6.484375 3.84375 -6.484375 C 4.03125 -6.484375 4.78125 -6.453125 4.78125 -5.9375 C 4.78125 -5.765625 4.703125 -5.625 4.671875 -5.578125 C 4.640625 -5.546875 4.609375 -5.5 4.609375 -5.46875 C 4.609375 -5.390625 4.6875 -5.390625 4.71875 -5.390625 C 5.015625 -5.390625 5.625 -5.78125 5.625 -6.34375 C 5.625 -6.9375 4.9375 -7.03125 4.5 -7.03125 C 3.140625 -7.03125 1.453125 -5.953125 1.453125 -4.734375 C 1.453125 -4.140625 1.890625 -3.78125 2.375 -3.625 Z M 2.375 -3.625 "/>
-</symbol>
-<symbol overflow="visible" id="glyph3-4">
-<path style="stroke:none;" d="M 3.53125 -6.8125 C 2.296875 -6.8125 1.765625 -6.578125 1.53125 -6.484375 C 0.515625 -6.0625 0.28125 -5.390625 0.28125 -5.25 C 0.28125 -5.1875 0.328125 -5.171875 0.390625 -5.171875 C 0.5625 -5.171875 1.046875 -5.421875 1.125 -5.640625 C 1.25 -6.015625 1.28125 -6.109375 1.9375 -6.203125 C 2.28125 -6.234375 2.609375 -6.265625 2.953125 -6.265625 L 3.859375 -6.265625 C 3.234375 -5.65625 2.9375 -4.578125 2.578125 -3.15625 C 2.296875 -1.96875 2.0625 -1.203125 1.65625 -0.671875 C 1.5625 -0.5625 1.546875 -0.546875 1.28125 -0.546875 L 0.640625 -0.546875 C 0.453125 -0.546875 0.34375 -0.546875 0.09375 -0.40625 C -0.015625 -0.34375 -0.234375 -0.171875 -0.234375 -0.0625 C -0.234375 -0.015625 -0.234375 0 -0.015625 0 L 3.40625 0 C 4.5625 0 5.4375 -0.875 5.4375 -1.21875 C 5.4375 -1.296875 5.359375 -1.296875 5.328125 -1.296875 C 5.15625 -1.296875 4.6875 -1.0625 4.578125 -0.8125 C 4.515625 -0.609375 4.484375 -0.546875 3.984375 -0.546875 L 2.078125 -0.546875 C 2.796875 -1.15625 3.09375 -2.140625 3.421875 -3.5 C 3.703125 -4.578125 3.9375 -5.546875 4.34375 -6.15625 C 4.40625 -6.25 4.421875 -6.265625 4.609375 -6.265625 L 5.46875 -6.265625 C 5.65625 -6.265625 5.75 -6.265625 6.015625 -6.40625 C 6.09375 -6.453125 6.328125 -6.625 6.328125 -6.734375 C 6.328125 -6.796875 6.3125 -6.8125 6.09375 -6.8125 Z M 3.53125 -6.8125 "/>
-</symbol>
-</g>
-</defs>
-<g id="surface1">
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-1" x="123.878" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="126.645" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-2" x="134.117" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph2-1" x="140.205" y="85.581"/>
-  <use xlink:href="#glyph2-2" x="143.318104" y="85.581"/>
-  <use xlink:href="#glyph2-3" x="147.288986" y="85.581"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-1" x="176.592" y="68.384"/>
-  <use xlink:href="#glyph0-3" x="179.35961" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="183.234" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="193.473" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="206.203" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="214.26" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-2" x="220.348" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="229.204" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="233.078" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="243.902" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="256.632" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="264.465" y="68.384"/>
-  <use xlink:href="#glyph0-2" x="268.339455" y="68.384"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph2-1" x="274.428" y="70.183"/>
-  <use xlink:href="#glyph2-4" x="277.541104" y="70.183"/>
-  <use xlink:href="#glyph2-3" x="281.511986" y="70.183"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 97.285156 -2.117188 L 220.429688 -2.117188 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-2" x="295.419" y="77.522"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-5" x="302.06" y="77.522"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-3" x="307.042" y="77.522"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="211.471" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="215.345" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="225.584" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="238.314" y="83.782"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="246.371" y="83.782"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 44.570312 -17.515625 L 185.550781 -17.515625 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="260.54" y="92.92"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-3" x="273.26224" y="92.92"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="183.033" y="98.515"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-1" x="338.217" y="83.118"/>
-  <use xlink:href="#glyph0-3" x="340.98461" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="344.859" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="355.099" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="367.829" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="375.885" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-2" x="381.973" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="390.829" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="394.703" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="405.527" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="418.257" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="426.09" y="83.118"/>
-  <use xlink:href="#glyph0-2" x="429.964455" y="83.118"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph2-1" x="436.053" y="84.916"/>
-  <use xlink:href="#glyph2-4" x="439.166104" y="84.916"/>
-  <use xlink:href="#glyph2-3" x="443.136986" y="84.916"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 258.910156 -16.851562 L 382.054688 -16.851562 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-2" x="457.044" y="92.256"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-6" x="463.686" y="92.256"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-3" x="468.667" y="92.256"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="372.915" y="98.515"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="376.79" y="98.515"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="387.614" y="98.515"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="400.344" y="98.515"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="408.177" y="98.515"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 103.726562 -31.199219 L 347.355469 -31.199219 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="422.346" y="106.602"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-3" x="435.06824" y="106.602"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="293.626" y="112.197"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 204.496094 -42.390625 L 246.589844 -42.390625 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="321.578" y="116.022"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-4" x="334.30024" y="116.022"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph2-1" x="339.732" y="117.821"/>
-  <use xlink:href="#glyph2-2" x="342.845104" y="117.821"/>
-  <use xlink:href="#glyph2-3" x="346.815986" y="117.821"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="283.801" y="123.389"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="294.041" y="123.389"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="306.771" y="123.389"/>
-</g>
-<path style="fill:none;stroke-width:0.3985;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 144.507812 -53.582031 L 306.574219 -53.582031 " transform="matrix(1,0,0,-1,72,72)"/>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="381.565" y="127.213"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-4" x="394.28724" y="127.213"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph2-1" x="399.72" y="129.012"/>
-  <use xlink:href="#glyph2-4" x="402.833104" y="129.012"/>
-  <use xlink:href="#glyph2-3" x="406.803986" y="129.012"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="223.814" y="135.244"/>
-  <use xlink:href="#glyph0-3" x="227.688455" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="231.563" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="241.802" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="254.532" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="262.589" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-2" x="268.677" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="277.533" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-2" x="281.407" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="292.231" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="304.961" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="312.794" y="135.244"/>
-  <use xlink:href="#glyph0-4" x="316.668455" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="323.31" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-3" x="336.04" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-1" x="339.914" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph3-1" x="350.154" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph1-3" x="362.884" y="135.244"/>
-</g>
-<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
-  <use xlink:href="#glyph0-4" x="370.717" y="135.244"/>
-</g>
-</g>
-</svg>