--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda.tex	Mon Feb 09 22:13:18 2015 +0900
@@ -0,0 +1,230 @@
+\chapter{Agda による証明手法}
+\label{chapter:agda}
+第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。
+その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。
+functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。
+例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。
+そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。
+
+そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。
+そのためにまずは Agda における証明手法について述べる。
+
+% {{{ Natural Deduction
+
+\section{Natural Deduction}
+\label{section:natural_deduction}
+証明には natural deduction(自然演繹)を用いる。
+natural deduction は Gentzen によって作られた論理と、その証明システムである。
+命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
+
+natural deduction において
+
+\begin{eqnarray}
+    \vdots \\ \nonumber
+    A \\ \nonumber
+\end{eqnarray}
+
+と書いた時、最終的に命題Aを証明したことを意味する。
+証明は木構造で表わされ、葉の命題は仮定となる。
+仮定には dead か alive の2つの状態が存在する。
+
+\begin{eqnarray}
+    \label{exp:a_implies_b}
+    A \\ \nonumber
+    \vdots \\ \nonumber
+    B \\ \nonumber
+\end{eqnarray}
+
+式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。
+この時 A は alive な仮定である。
+証明された B は A の仮定に依存していることを意味する。
+
+ここで、推論規則により記号 $ \Rightarrow $ を導入する。
+
+\begin{prooftree}
+    \AxiomC{[$ A $]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \Rightarrow \mathcal{I} $}
+    \UnaryInfC{$ A \Rightarrow B $}
+\end{prooftree}
+
+そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
+A という仮定に依存して B を導く証明から、A が存在すれば B が存在するという証明を導いたこととなる。
+このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。
+
+alive な仮定を dead にすることができるのは $ \Rightarrow I $ 規則のみである。
+それを踏まえ、 natural deduction には以下のような規則が存在する。
+
+\begin{itemize}
+    \item Hypothesis
+
+        仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。
+
+        $ A $
+
+    \item Introductions
+
+        導入。証明された論理式に対して記号を導入することで新たな証明を導く。
+
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \land \mathcal{I} $}
+    \BinaryInfC{$ A \land B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+    \RightLabel{ $ \lor 1 \mathcal{I} $}
+    \UnaryInfC{$ A \lor B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \lor 2 \mathcal{I} $}
+    \UnaryInfC{$ A \lor B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{[$ A $]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \Rightarrow \mathcal{I} $}
+    \UnaryInfC{$ A \Rightarrow B $}
+\end{prooftree}
+
+\item Eliminations
+
+    除去。ある論理記号で構成された証明から別の証明を導く。
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \land B $ }
+    \RightLabel{ $ \land 1 \mathcal{E} $}
+    \UnaryInfC{$ A $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \land B $ }
+    \RightLabel{ $ \land 2 \mathcal{E} $}
+    \UnaryInfC{$ B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \lor B $ }
+
+    \AxiomC{[$A$]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ C $ }
+
+    \AxiomC{[$B$]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ C $ }
+
+    \RightLabel{ $ \lor \mathcal{E} $}
+    \TrinaryInfC{ $ C $ }
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \Rightarrow B $ }
+
+    \RightLabel{ $ \Rightarrow \mathcal{E} $}
+    \BinaryInfC{$ B $}
+\end{prooftree}
+
+\end{itemize}
+
+記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
+natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。
+
+それぞれの記号は以下のような意味を持つ
+\begin{itemize}
+    \item $ \land $
+        conjunction。2つの命題が成り立つことを示す。
+        $ A \land B $ と記述すると A かつ B と考えることができる。
+
+    \item $ \lor $
+        disjunction。2つの命題のうちどちらかが成り立つことを示す。
+        $ A \lor B $ と記述すると A または B と考えることができる。
+
+    \item $ \Rightarrow $
+        implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
+        $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。
+\end{itemize}
+
+例として、natural deduction で三段論法を証明する。
+なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。
+
+\begin{prooftree}
+    \AxiomC{ $ [A] $ $_{(1)}$}
+    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
+    \RightLabel{ $ \land 1 \mathcal{E} $ }
+    \UnaryInfC{ $ (A \Rightarrow B) $ }
+    \BinaryInfC{ $ B $ }
+
+    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
+    \RightLabel{ $ \land 2 \mathcal{E} $ }
+    \UnaryInfC{ $ (B \Rightarrow C) $ }
+
+    \BinaryInfC{ $ C $ }
+    \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
+    \UnaryInfC{ $ A \Rightarrow C $}
+    \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
+    \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
+\end{prooftree}
+
+まず、三段論法を論理式で表す。
+
+「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。
+まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。
+次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。
+そしてこの2つは同時に成り立つ。
+よって  $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。
+この条件2つが成り立つ時に「Aは Cである」が成りたつ。
+条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ になる。
+
+証明の手順はこうである。
+まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAを2つ仮定する。
+条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。
+A と $ A \Rightarrow B$ から B を、 B から $ B \Rightarrow C $ から C を導く。
+ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。
+この際に dead にする仮定は A である。
+そのために $_{(1)} $ と対応する \verb/[]/の記号に数値を付けてある。
+これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。
+結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。
+
+% }}}
+
+\section{Curry-Howard Isomorphism}
+\section{Agda による証明}
+\section{Reasoning}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bussproofs.sty	Mon Feb 09 22:13:18 2015 +0900
@@ -0,0 +1,1136 @@
+%
+\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/future.tex	Mon Feb 09 11:17:00 2015 +0900
+++ b/future.tex	Mon Feb 09 22:13:18 2015 +0900
@@ -1,1 +1,1 @@
-\chapter{今後の課題}
+\chapter{まとめと今後の課題}

--- a/main.tex	Mon Feb 09 11:17:00 2015 +0900
+++ b/main.tex	Mon Feb 09 22:13:18 2015 +0900
@@ -4,6 +4,7 @@
 \usepackage{multirow}
 \usepackage{here}
 \usepackage{listings}
+\usepackage{bussproofs}
 
 \setlength{\itemsep}{-1zh}
 \title{圏によるプログラムの変更の形式化}
@@ -71,12 +72,7 @@
 \pagenumbering{arabic}
 \input{delta}
 \input{category}
-
-\chapter{Agda による証明手法}
-\section{Natural Deduction}
-\section{Curry-Howard Isomorphism}
-\section{Agda による証明}
-\section{Reasoning}
+\input{agda}
 
 \chapter{Delta が Monad である証明}
 \section{Agda における Functor 則}
@@ -88,8 +84,6 @@
 \section{Monad と組み合せた Delta である DeltaM の定義}
 \section{DeltaM が Monad 則を満たす証明}
 
-\chapter{結論}
-
 % 今後の課題
 \input{future.tex}