Mercurial > hg > Papers > 2018 > hamase_midterm
changeset 0:c9b5432397b7
first commit
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/Makefile Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,36 @@ +# Created by Daichi Toma on Nov 16, 2011 + +TARGET=midterm + +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 *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/bussproofs.sty Thu Nov 08 10:57:19 2018 +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 +} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/dummy.tex Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,61 @@ + +%%% 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/fancyhdr.sty Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,236 @@ +%% +%% 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'.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/jlisting.sty Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,216 @@ +\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}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.aux Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,22 @@ +\relax +\citation{Yasutaka:2016} +\citation{agda} +\@writefile{toc}{\contentsline {section}{\numberline {1}研究目的}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}} +\newlabel{src:singlelinked}{{1}{1}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCによるStack}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {3}Agda}{1}} +\citation{*} +\bibstyle{junsrt} +\bibdata{reference} +\bibcite{Yasutaka:2016}{1} +\bibcite{agda}{2} +\bibcite{Tatsuki:2016}{3} +\bibcite{kaito:2015}{4} +\bibcite{agda-documentation}{5} +\newlabel{src:stack-agda}{{2}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}AgdaによるStack}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {4}RedBlackTree}{2}} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces RedBlackTreeの例}}{2}} +\newlabel{fig:rbtree}{{1}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {5}今後の課題}{2}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.bbl Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,25 @@ +\begin{thebibliography}{1} + +\bibitem{Yasutaka:2016} +{比嘉 健太, 河野 真治}. +\newblock {メタ計算を用いた Continuation based C の検証手法}, 2016. + +\bibitem{agda} +The agda wiki. +\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. +\newblock Accessed: 2017/10/24(Tue). + +\bibitem{Tatsuki:2016} +{伊波 立樹, 東恩納 琢偉, 河野 真治}. +\newblock {Code Gear 、Data Gear に基づく OS のプロトタイプ}, 2016. + +\bibitem{kaito:2015} +{徳森 海斗, 河野 真治}. +\newblock {LLVM Clang 上の Continuation based C コンパイラ の改良}, 2015. + +\bibitem{agda-documentation} +Welcome to agda’s documentation! ― agda 2.6.0 documentation. +\newblock \url{http://agda.readthedocs.io/en/latest/index.html}. +\newblock Accessed: 2017/10/24(Tue). + +\end{thebibliography}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.blg Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,47 @@ +This is pBibTeX, Version 0.99d-j0.33 (utf8.euc) (TeX Live 2018) +Capacity: max_strings=100000, hash_size=100000, hash_prime=85009 +The top-level auxiliary file: midterm.aux +The style file: junsrt.bst +Database file #1: reference.bib +You've used 5 entries, + 2270 wiz_defined-function locations, + 561 strings with 4741 characters, +and the built_in function-call counts, 806 in all, are: += -- 44 +> -- 14 +< -- 0 ++ -- 8 +- -- 3 +* -- 5 +:= -- 87 +add.period$ -- 12 +call.type$ -- 5 +change.case$ -- 5 +chr.to.int$ -- 0 +cite$ -- 5 +duplicate$ -- 55 +empty$ -- 121 +format.name$ -- 6 +if$ -- 201 +int.to.chr$ -- 0 +int.to.str$ -- 5 +missing$ -- 0 +newline$ -- 25 +num.names$ -- 3 +pop$ -- 63 +preamble$ -- 1 +purify$ -- 0 +quote$ -- 0 +skip$ -- 47 +stack$ -- 0 +substring$ -- 0 +swap$ -- 5 +text.length$ -- 0 +text.prefix$ -- 0 +top$ -- 0 +type$ -- 0 +warning$ -- 0 +while$ -- 3 +width$ -- 6 +write$ -- 44 +is.kanji.str$ -- 33
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.log Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,258 @@ +This is e-pTeX, Version 3.14159265-p3.8.0-180226-2.6 (utf8.euc) (TeX Live 2018) (preloaded format=platex 2018.11.8) 8 NOV 2018 10:52 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**midterm.tex +(./midterm.tex +pLaTeX2e <2018-04-01>+1 (based on LaTeX2e <2018-04-01> patch level 2) +Babel <3.18> and hyphenation patterns for 84 language(s) loaded. +(/usr/local/texlive/2018/texmf-dist/tex/platex/base/jarticle.cls +Document Class: jarticle 2018/02/04 v1.7h Standard pLaTeX class +\c@@paper=\count83 +(/usr/local/texlive/2018/texmf-dist/tex/platex/base/jsize10.clo +File: jsize10.clo 2018/02/04 v1.7h Standard pLaTeX file (size option) +) +\c@part=\count84 +\c@section=\count85 +\c@subsection=\count86 +\c@subsubsection=\count87 +\c@paragraph=\count88 +\c@subparagraph=\count89 +\c@figure=\count90 +\c@table=\count91 +\abovecaptionskip=\skip41 +\belowcaptionskip=\skip42 +\symmincho=\mathgroup4 +LaTeX Font Info: Overwriting symbol font `mincho' in version `bold' +(Font) JY1/mc/m/n --> JY1/gt/m/n on input line 614. +\toclineskip=\dimen118 +\@lnumwidth=\dimen119 +\bibindent=\dimen120 +\heisei=\count92 +) +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2017/06/01 v1.1a Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/10/28 v1.15 key=value parser (DPC) +\KV@toks@=\toks15 +) +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2017/06/25 v1.2c Standard LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2016/01/03 v1.10 sin cos tan (DPC) +) +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: dvipdfmx.def on input line 99. + +(/usr/local/texlive/2018/texmf-dist/tex/latex/graphics-def/dvipdfmx.def +File: dvipdfmx.def 2017/06/24 v5.0g Graphics/color driver for dvipdfmx +)) +\Gin@req@height=\dimen121 +\Gin@req@width=\dimen122 +) +(./picins.sty Option `picins' Version 3.0 Sep. 1992, TH Darmstadt/HRZ +\@BILD=\box42 +\@TEXT=\box43 +\d@breite=\dimen123 +\d@hoehe=\dimen124 +\d@xoff=\dimen125 +\d@yoff=\dimen126 +\d@shad=\dimen127 +\d@dash=\dimen128 +\d@boxl=\dimen129 +\d@pichskip=\dimen130 +\d@tmp=\dimen131 +\d@tmpa=\dimen132 +\d@bskip=\dimen133 +\hsiz@=\dimen134 +\p@getot@l=\dimen135 +\c@breite=\count93 +\c@hoehe=\count94 +\c@xoff=\count95 +\c@yoff=\count96 +\c@pos=\count97 +\c@shad=\count98 +\c@dash=\count99 +\c@boxl=\count100 +\c@zeilen=\count101 +\@changemode=\count102 +\c@piccaption=\count103 +\c@piccaptionpos=\count104 +\c@picpos=\count105 +\c@whole=\count106 +\c@half=\count107 +\c@tmp=\count108 +\c@tmpa=\count109 +\c@tmpb=\count110 +\c@tmpc=\count111 +\c@tmpd=\count112 +\d@leftskip=\skip43 +\ptoti=\dimen136 +\ptotii=\dimen137 +\env@box=\box44 +\d@envdp=\dimen138 +\c@hsize=\count113 +\c@envdp=\count114 +\d@envb=\dimen139 +) +(./fancyhdr.sty +Package: fancyhdr 2017/06/30 v3.9a Extensive control of page headers and footer +s +\f@nch@headwidth=\skip44 +\f@nch@O@elh=\skip45 +\f@nch@O@erh=\skip46 +\f@nch@O@olh=\skip47 +\f@nch@O@orh=\skip48 +\f@nch@O@elf=\skip49 +\f@nch@O@erf=\skip50 +\f@nch@O@olf=\skip51 +\f@nch@O@orf=\skip52 +) (/usr/local/texlive/2018/texmf-dist/tex/latex/url/url.sty +\Urlmuskip=\muskip10 +Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. +) +(./bussproofs.sty +Proof Tree (bussproofs) style macros. Version 1.1. +\theLevel=\count115 +\myMaxLevel=\count116 +\myBoxA=\box45 +\myBoxB=\box46 +\myBoxC=\box47 +\myBoxD=\box48 +\myBoxLL=\box49 +\myBoxRL=\box50 +\thisAboveSkip=\dimen140 +\thisBelowSkip=\dimen141 +\newScoreStart=\dimen142 +\newScoreEnd=\dimen143 +\newCenter=\dimen144 +\displace=\dimen145 +\leftLowerAmt=\dimen146 +\rightLowerAmt=\dimen147 +\scoreHeight=\dimen148 +\scoreDepth=\dimen149 +\htLbox=\dimen150 +\htRbox=\dimen151 +\htRRbox=\dimen152 +\htRRRbox=\dimen153 +\htAbox=\dimen154 +\htCbox=\dimen155 +) (/usr/local/texlive/2018/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count117 +\lst@gtempboxa=\box51 +\lst@token=\toks16 +\lst@length=\count118 +\lst@currlwidth=\dimen156 +\lst@column=\count119 +\lst@pos=\count120 +\lst@lostspace=\dimen157 +\lst@width=\dimen158 +\lst@newlines=\count121 +\lst@lineno=\count122 +\lst@maxwidth=\dimen159 + +(/usr/local/texlive/2018/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2015/06/04 1.6 (Carsten Heinz) +\c@lstnumber=\count123 +\lst@skipnumbers=\count124 +\lst@framebox=\box52 +) +(/usr/local/texlive/2018/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2015/06/04 1.6 listings configuration +)) +Package: listings 2015/06/04 1.6 (Carsten Heinz) + +(./jlisting.sty +Package: jlisting 2006/02/20 0.2 (Thor) +\lst@nextchar=\count125 +\lst@inputfile=\read1 +) (./dummy.tex) + +LaTeX Warning: Unused global option(s): + [9.5pt]. + +(./midterm.aux) +\openout1 = `midterm.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 41. +LaTeX Font Info: ... okay on input line 41. +\c@lstlisting=\count126 +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <12> on input line 45. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <8> on input line 45. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <6> on input line 45. +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <14.4> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 48. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <14.4> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 48. +LaTeX Font Info: Try loading font information for OMS+cmr on input line 113. + + (/usr/local/texlive/2018/texmf-dist/tex/latex/base/omscmr.fd +File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions +) +LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available +(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 113. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <7> on input line 113. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <5> on input line 113. +LaTeX Font Info: Try loading font information for OML+cmr on input line 113. + + +(/usr/local/texlive/2018/texmf-dist/tex/latex/base/omlcmr.fd +File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions +) +LaTeX Font Info: Font shape `OML/cmr/m/n' in size <10> not available +(Font) Font shape `OML/cmm/m/it' tried instead on input line 113. + +Underfull \hbox (badness 1275) in paragraph at lines 125--128 +[]\JY1/mc/m/n/10 比嘉 \OT1/cmr/m/n/10 (2016)[[]] \JY1/mc/m/n/10 では \OT1/cmr/m +/n/10 CbC \JY1/mc/m/n/10 における \OT1/cmr/m/n/10 Code-Seg-ment \JY1/mc/m/n/10 +、 + [] + +File: ../pic/emblem-bitmap.pdf Graphic file (type pdf) +<../pic/emblem-bitmap.pdf> + +Package Fancyhdr Warning: \headheight is too small (0.0pt): + Make it at least 20.37784pt. + We now make it that large for the rest of the document. + This may cause the page layout to be inconsistent, however. + +[1 + + +] +File: ../pic/rbtree.pdf Graphic file (type pdf) +<../pic/rbtree.pdf> + (./midterm.bbl) [2] (./midterm.aux) ) +Here is how much of TeX's memory you used: + 2841 strings out of 493281 + 35755 string characters out of 6145041 + 272533 words of memory out of 5000000 + 6775 multiletter control sequences out of 15000+600000 + 13256 words of font info for 52 fonts, out of 8000000 for 9000 + 929 hyphenation exceptions out of 8191 + 37i,16n,45p,369b,1854s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on midterm.dvi (2 pages, 17680 bytes).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.tex Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,338 @@ +\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{CbC言語によるプログラムの検証} +\author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治} +\date{} +\maketitle +\thispagestyle{fancy} + +\section{研究目的} + +%% Agdaのお勉強のこと、CbCをAgdaに直したこと、CbC側のDeletionのこと + +%% CbC でソフトウェアを検証できるかを CbCで書いた RBTree と Agda で同様に書いた RBTree を検証することで示す + +%% ソフトウェアの規模が大きくなるにつれて期待されない動作をすることが増える。ここでは期待される動作を仕様、期待されない動作をバグと呼ぶことにする。 +%% それにはソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 +%% 期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 + +%% 特に実際に動作するソフトウェアを検証、証明できることが望ましい。 +%% そのために当研究室では CodeSegment 、 Data Segment という単位を用いてソフトウェアを記述する手法を提案している。 +%% 処理の単位である CodeSegment は、メタ計算によって相互に接続される。 +%% メタ計算を切り替えることで CodeSegment を変更することなくソフトウェアの性質を検証することができる。 +% CbC検証と実装が同一の言語で行える言語である。 +% CbCの特徴はだいじょうぶ？完全じゃなくていいけどある程度は乗せなきゃ駄目だよね + +ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。 +モデル検査はソフトウェアの状態をすべて数え上げ、すべての状態で仕様が正しいことを確認する方法である。 +定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明することである。%% atton-master papar より +%% モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。 +%% そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。 +%% 検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。 + +% この問題を解決する為に +当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。 +本研究では、検証や証明に直接使用できる言語として CbC を用いる。 + + %% CbC 上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法は、比嘉(2016)\cite{Yasutaka:2016}により提案、実装されている。 +%% また、赤黒木の仕様が、限定的な木の大きさの範囲内で検証されている。 + +%% 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。 + +%% プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。 + +%% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。 + +本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検証、証明する。 + +%%検証と証明の話書かないとAgda出せなくない？ + +\section{Countinuation based C (CbC)} +Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。 +CbC では OS や組み込みソフトウェアを主な対象としている。 +CbC は C 言語とほぼおなじ構文を持ち、よりアセンブラに近い形でプログラムを記述する。 + +CbC では C の関数の代わりに CodeSegment を用いて処理を記述する。 +CodeSegment は値を入力として受取り、出力を行う処理の単位で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 +CbC の CodeSegment を定義するには C とは少し異なり関数定義のの先頭に \_\_code が付く。 +DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。CodeSegment の入力となる DataSegment は Input DataSegment 出力 を Input DataSegment は関数の引数として定義する。次の CodeSegment に処理を移す際は、 goto の後に CodeSegment 名と Input DataDataSegment を指定する。 +% 図\ref{fig:CSContinuation}は CodeSegment 感の処理の流れを表している。 + +%%% figure +%% \begin{figure}[htbp] +%% \begin{center} +%% \includegraphics[width=60mm]{../pic/codesegment.pdf} +%% \end{center} +%% \caption{ goto による CodeSegment 間の接続} +%% \label{fig:CSContinuation} +%% \end{figure} + +CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。 +例として CbC による Stack に対する操作のコード示す。 + +\newpage +\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace} + +このコードでは Stack に対する push と pop を定義している。 + +push や pop は必要があるときに外から呼ばれる。 + +push では element で新しい要素を作って、次の要素との関係、 push する要素を入れ、Stack の top を書き換えて次のCodeSegmentに飛ぶ。 + +pop では Stack の top に data があればその data を next に入れ、次のCodeSegmentに飛ぶ。 top に data が無ければ NULL を next の Input Data に入れて次のCodeSegmentに飛ぶ。 + +%% また CbC で Functional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。 + +比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。 +これより、 CbC で Functional に書かれたプログラムは等価な Agda のコードの置き換えることができる。 +本研究では CbC の代わりに等価なAgdaのコードに変換することで証明を行う。 + +\section{Agda} +Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。 +依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 + +CbC を Agda に変換する場合 DataSegment をレコード型、 CodeSegment は関数型となる。 + +前項で示した CbC で書かれた Stack の操作をAgda に変換したコードを示す。 + +\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace} + +%CbC で書かれた Stack の CodeSegment が要素、Tree、 + +Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。 +%% 引数は変数で受けることもできるが、具体的な型構築子を渡された時の挙動を定義することができる。これはパターンマッチと呼ばれ、型構築子で case 文を行っているようなものである。 +%% パターンマッチはすべての場合を含む必要があり、特定のものだけ異なる挙動にしたい場合は構築子を幾つか指定した後に変数で受けることで解決できる。なお、マッチした値を変数として利用しない場合は _ で値を捨てることもできる。 + +関数にはリテラルが存在し、関数を定義せずにその場で値を生成することもできる。これは ラムダ式と呼ばれ、 \verb/\arg1 arg2 -> function body/ または $ \lambda $ arg1 arg2 → function body のように記述できる。上の例では pushStack の \verb/\s1 -> next (record {stack = s1})/ や、 popStack の \verb/\s1 -> next s0/ が ラムダ式である。 + + +%%%%%%%% + Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコードを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙していく。複数の値を列挙する際は ; で区切る。上の例では \verb/record {stack = s1}/ がそれにあたる。 + + + +%% リテラル is 何 + + +%% このコードでは push 、 pop の関数を定義をしている。 +%% push では要素を追加した新しいStackを返す。 +%% pop では data があればそのデータを pop し、しない場合はそもそも + +このように CbC のコードを Agda に変換し、証明を行う。 + + +% 証明を行う前に自然演繹について説明 +%% 自然演繹とは Gentzen によって作られた論理とその証明システムである。命題変数と記号を用いた論理式で論理を記述し、推論規則を使って変形することで求める論理式を導く。 + +%% 始めに、自然演繹と型付き$ \lambda $ 計算の対応を定義する。 +%% \begin{center} +%% \begin{table}[htbp] +%% \scalebox{0.75}{ +%% \begin{tabular}{|c|c|} \hline +%% Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline +%% $ A $ & 型 A を持つ変数 x \\ \hline +%% $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline +%% $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline +%% $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline +%% $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline +%% $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline +%% $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline +%% $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline +%% \end{tabular} +%% } +%% \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} +%% \label{table:curry} +%% \end{table} +%% \end{center} + +%% ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 + +%% この三段論法を自然演繹による証明木にすると次のようになる。 + +%% \begin{figure}[htpb] +%% \begin{center} +%% \includegraphics[width=95mm]{../pic/modus-ponens.pdf} +%% \end{center} +%% \caption{自然演繹での三段論法の証明} +%% \label{fig:modus-ponens} +%% \end{figure} + + +%% この証明木に対応するAgdaによる証明は次のようになる。 + +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% data _×_ (A B : Set) : Set where +%% <_,_> : A → B → A × B + +%% fst : {A B : Set} → A × B → A +%% fst < a , _ > = a + +%% snd : {A B : Set} → A × B → B +%% snd < _ , b > = b + + +%% f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) +%% f = λ p x → (snd p) ((fst p) x) +%% \end{lstlisting} + +%% 三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。 + +%% $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 +%% よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 +%% %% これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 +%% 仮定 $ (A \rightarrow B) \times (B \rightarrow C) $ と仮定 A から A $ \rightarrow $ C を導いている。 + +%% 仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。 +%% fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。 +%% もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。 +%% 得られた B を snd p に適用することで最終的に C が導ける。 + +%% \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced} + +%% このように Agda では証明を記述することができる。 + +% Agdaの知識ってどう出す？ + +%TODO 定理証明とプログラムの話 + +%% \begin{prooftree} +%% \AxiomC{ $ [A] $ $_{(1)}$} +%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } +%% \RightLabel{ $ \land 1 \mathcal{E} $ } +%% \UnaryInfC{ $ (A \Rightarrow B) $ } +%% \RightLabel{ $ \Rightarrow \mathcal{E} $} +%% \BinaryInfC{ $ B $ } + + +%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } +%% \RightLabel{ $ \land 2 \mathcal{E} $ } +%% \UnaryInfC{ $ (B \Rightarrow C) $ } + +%% \RightLabel{ $ \Rightarrow \mathcal{E} $} +%% \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} + + +%% Agdaによる三段論法の証明 + +%% 定理証明支援器では Curry-Howard 同型対応により書いた命題通りに書いたプログラムをコンパイルが通ることはその命題を証明することが等しい。 + +%% 以下に CbC で書かれた Stack の 定義の一部と それを Agda に変換したものの定義の一部分を示す。 +%% push だけじゃなく pop も入れたほうがいい…のかな + +%%% CbCのCodeSegmentの例 + +%% context.h + + +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% \end{lstlisting} + + % Stack.agdaのコード +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% record Stack {a t : Set} (stackImpl : Set) : Set where +%% field +%% stack : stackImpl +%% push : stackImpl -> a -> (stackImpl -> t) -> t + +%% pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t +%% pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) +%% \end{lstlisting} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\section{RedBlackTree} +RedBlackTree とは拡張された二分探索木で、木のバランスを取るための情報として各ノードにそれぞれ赤、黒の色を持っている。 +また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。 +%%RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。 + +%% \begin{itemize} +%% \item 各ノードは赤か黒の色を持つ。 +%% \item ルートノードの色は黒である。 +%% \item 葉ノードの色は黒である。 +%% \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。 +%% \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 +%% \end{itemize} + +数値を要素に持つ RedBlackTree の例を以下の図\ref{fig:rbtree}に示す。 +条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。 +加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 +%% atton-master fig3.1 + +%%%%figure +\begin{figure}[htpb] + \begin{center} + \includegraphics[width=50mm]{../pic/rbtree.pdf} + \end{center} + \caption{RedBlackTreeの例} + \label{fig:rbtree} +\end{figure} + +本研究で検証する RedBlackTree は非破壊であり、一度構築した木構造は破壊される操作ごとに新しい木が生成される。非破壊である理由は並列実行時のデータ保存である。 + + +%% atton-master@13p + +%% figure +%\begin{figure}[htbp] +% \begin{center} +% \includegraphics[width=50mm]{../pic/treeVnc.pdf} +% \end{center} +% \caption{構成される木構造} +% \label{fig:tree} +%\end{figure} + +%% \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} + +\section{今後の課題} +現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。 +今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。 + +\nocite{*} +\bibliographystyle{junsrt} +\bibliography{reference} +\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/Makefile Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,37 @@ +# 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/bussproofs.sty Thu Nov 08 10:57:19 2018 +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 +} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/modus-ponens.svg Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,322 @@ +<?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>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/modus-ponens.tex Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,56 @@ +% {{{ settings +% vim:set fileencoding=utf8: +\documentclass[10pt]{jarticle} + +\usepackage{amsmath} +\usepackage{cprotect} +\usepackage{listings} +\usepackage{moreverb} +\usepackage{url} +\usepackage{bussproofs} +\usepackage[dvipdfmx]{graphicx} + +% equation number with section number +\makeatletter +\renewcommand{\theequation}{\arabic{section}-\arabic{equation}} +\@addtoreset{equation}{section} +\makeatother + +\setlength{\textwidth}{179mm} +\setlength{\textheight}{251mm} +\setlength{\topmargin}{-2cm} +\setlength{\oddsidemargin}{-1cm} +\setlength{\evensidemargin}{-1cm} + +% }}} + +\pagenumbering{gobble} + +\begin{document} + +\title{} +\author{} +\date{} + +\begin{prooftree} + \AxiomC{ $ [A] $ $_{(1)}$} + \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } + \RightLabel{ $ \land 1 \mathcal{E} $ } + \UnaryInfC{ $ (A \Rightarrow B) $ } + \RightLabel{ $ \Rightarrow \mathcal{E} $} + \BinaryInfC{ $ B $ } + + \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } + \RightLabel{ $ \land 2 \mathcal{E} $ } + \UnaryInfC{ $ (B \Rightarrow C) $ } + + \RightLabel{ $ \Rightarrow \mathcal{E} $} + \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} + +\end{document} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/picins.sty Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,578 @@ +% PICINS.STY --- Style File zum Einbinden von Bildern +% Autor: J. Bleser, E. Lang +% Hochschulrechenzentrum +% Technische Hochschule Darmstadt +% !!! Dieses Style-File ist urheberrechtlich geschuetzt !!! +% !!! Aenderungen nur mit Zustimmung der Autoren !!! +\message{Option `picins' Version 3.0 Sep. 1992, TH Darmstadt/HRZ} +\newbox\@BILD% +\newbox\@TEXT% +\newdimen\d@breite% +\newdimen\d@hoehe% +\newdimen\d@xoff% +\newdimen\d@yoff% +\newdimen\d@shad% +\newdimen\d@dash% +\newdimen\d@boxl% +\newdimen\d@pichskip% +\newdimen\d@tmp +\newdimen\d@tmpa +\newdimen\d@bskip +\newdimen\hsiz@% +\newdimen\p@getot@l% +\newcount\c@breite +\newcount\c@hoehe +\newcount\c@xoff +\newcount\c@yoff +\newcount\c@pos +\newcount\c@shad +\newcount\c@dash +\newcount\c@boxl +\newcount\c@zeilen% +\newcount\@changemode% +\newcount\c@piccaption% +\newcount\c@piccaptionpos% +\newcount\c@picpos +\newcount\c@whole% +\newcount\c@half% +\newcount\c@tmp +\newcount\c@tmpa +\newcount\c@tmpb +\newcount\c@tmpc +\newcount\c@tmpd +\newskip\d@leftskip +\newif\if@list \@listfalse% +\newif\if@offset% + + +\c@piccaptionpos=1% +\c@picpos=0 +\d@shad=4pt% +\d@dash=4pt% +\d@boxl=10pt% +\d@pichskip=1em% +\@changemode=0% +\def\@captype{figure}% +\let\old@par=\par% + +\def\pichskip#1{\d@pichskip #1\relax} + + +\def\shadowthickness#1{\d@shad #1\relax} + + +\def\dashlength#1{\d@dash #1\relax} + + +\def\boxlength#1{\d@boxl #1\relax} + + +\def\picchangemode{\@changemode=1}% +\def\nopicchangemode{\@changemode=0}% + + +\def\piccaptionoutside{\c@piccaptionpos=1}% +\def\piccaptioninside{\c@piccaptionpos=2}% +\def\piccaptionside{\c@piccaptionpos=3}% +\def\piccaptiontopside{\c@piccaptionpos=4}% + +\def\piccaption{\@ifnextchar [{\@piccaption}{\@piccaption[]}} +\def\@piccaption[#1]#2{\c@piccaption=1\def\sh@rtf@rm{#1}\def\capti@nt@xt{#2}} +\def\make@piccaption{% + \hsiz@\d@breite% + \ifnum\c@piccaptionpos=2% + \advance\hsiz@ -2\fboxsep% + \fi% + \ifnum\c@piccaptionpos>2% + \hsiz@\hsize\advance\hsiz@-\d@breite\advance\hsiz@-\d@pichskip% + \fi% + \setbox\@TEXT=\vbox{\hsize\hsiz@\caption[\sh@rtf@rm]{\capti@nt@xt}}% +} + + + +\def\newcaption{\refstepcounter\@captype\@dblarg{\@newcaption\@captype}} +\long\def\@newcaption#1[#2]#3{% + \old@par% + \addcontentsline{\csname ext@#1\endcsname }{#1}% + {\protect\numberline{\csname the#1\endcsname}{\ignorespaces #2}} + \begingroup\@parboxrestore\normalsize% + \@newmakecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\old@par% + \endgroup% +} +\long\def\@newmakecaption#1#2{% + \vskip 10pt% + \setbox\@tempboxa \hbox {#1: #2}% + \ifdim \wd\@tempboxa >\hsize% + \setbox0=\hbox{#1: }\dimen0=\hsize\advance\dimen0 by-\wd0 + \setbox1=\vtop{\hsize=\dimen0 #2} + \hbox{\box0 \box1} + \par + \else \hbox to\hsize {\hfil \box \@tempboxa \hfil} + \fi +} + + + + + +\def\parpic{% + \@ifnextchar ({\iparpic}{\iparpic(0pt,0pt)} +} +\def\iparpic(#1,#2){% + \@ifnextchar ({\@offsettrue\iiparpic(#1,#2)}% + {\@offsetfalse\iiparpic(#1,#2)(0pt,0pt)} +} +\def\iiparpic(#1,#2)(#3,#4){% + \@ifnextchar [{\iiiparpic(#1,#2)(#3,#4)}{\iiiparpic(#1,#2)(#3,#4)[l]} +} +\def\iiiparpic(#1,#2)(#3,#4)[#5]{% + \@ifnextchar [{\ivparpic(#1,#2)(#3,#4)[#5]}{\ivparpic(#1,#2)(#3,#4)[#5][]} +} +\def\ivparpic(#1,#2)(#3,#4)[#5][#6]#7{% + \let\par=\old@par\par% + \hangindent0pt\hangafter1% + \setbox\@BILD=\hbox{#7}% + \d@breite=#1\d@breite=\the\d@breite% + \ifdim\d@breite=0pt\d@breite=\wd\@BILD\fi% + \c@breite=\d@breite\divide\c@breite by65536% + \multiply\c@piccaption\c@piccaptionpos% + \d@hoehe=#2\d@hoehe=\the\d@hoehe% + \ifdim\d@hoehe=0pt\d@hoehe=\ht\@BILD\advance\d@hoehe by\dp\@BILD\fi% + \c@hoehe=\d@hoehe\divide\c@hoehe by65536% + \d@xoff=#3\c@xoff=\d@xoff\divide\c@xoff by65536% + \d@yoff=\d@hoehe% + \advance\d@yoff by-#4\c@yoff=\d@yoff\divide\c@yoff by65536% + \c@pos=1\unitlength1pt% + \if@offset% + \setbox\@BILD=\hbox{% + \begin{picture}(\c@breite,\c@hoehe)% + \put(0,0){\makebox(\c@breite,\c@hoehe){}}% + \put(\c@xoff,\c@yoff){\box\@BILD}% + \end{picture}% + }% + \else% + \setbox\@BILD=\hbox{% + \begin{picture}(\c@breite,\c@hoehe)% + \put(0,0){\makebox(\c@breite,\c@hoehe)[#6]{\box\@BILD}}% + \end{picture}% + }% + \fi% + \ifnum\c@piccaption=2% + \make@piccaption% + \advance\d@hoehe\ht\@TEXT\advance\d@hoehe\dp\@TEXT% + \c@hoehe=\d@hoehe\divide\c@hoehe by65536% + \setbox\@BILD=\vbox{\box\@BILD\vspace{-5pt}% + \hbox{\hspace{\fboxsep}\box\@TEXT}% + \vspace{4pt}}% + \fi% + \@tfor\@tempa := #5\do{% + \if\@tempa f\setbox\@BILD=\hbox{\Rahmen(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa s\setbox\@BILD=\hbox{\Schatten(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa o\setbox\@BILD=\hbox{\Oval(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa d\setbox\@BILD=\hbox{\Strich(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa x\setbox\@BILD=\hbox{\Kasten(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa l\c@pos=1\fi% + \if\@tempa r\c@pos=2\fi% + }% + \ifnum\c@piccaption=1% + \make@piccaption% + \advance\d@hoehe\ht\@TEXT\advance\d@hoehe\dp\@TEXT% + \c@hoehe=\d@hoehe\divide\c@hoehe by65536% + \setbox\@BILD=\vbox{\box\@BILD\vspace{-5pt}\hbox{\box\@TEXT}\vspace{4pt}}% + \fi% + \ifodd\count0\c@picpos=0\else\c@picpos=\@changemode\fi% + \pagetotal=\the\pagetotal% + \d@tmp=\pagegoal\advance\d@tmp by-\pagetotal\advance\d@tmp by-\baselineskip% + \ifdim\d@hoehe>\d@tmp% + \vskip 0pt plus\d@hoehe\relax\pagebreak[3]\vskip 0pt plus-\d@hoehe\relax% + \ifnum\c@picpos=1\c@picpos=0\else\c@picpos=\@changemode\fi% + \fi% + \ifnum\c@picpos=1\ifnum\c@pos=1\c@pos=2\else\c@pos=1\fi\fi% + \ifnum\@listdepth>0 + \@listtrue\parshape 0% + \advance\hsize -\rightmargin% + \d@leftskip \leftskip% + \leftskip \@totalleftmargin% + \if@inlabel\rule{\linewidth}{0pt}\vskip-\baselineskip\relax\fi% + \else\@listfalse\medskip% + \fi% + \if@list\d@tmpa=\linewidth\else\d@tmpa=\hsize\fi% + \ifnum\c@piccaption=3% + \make@piccaption% + \d@tmp\ht\@TEXT\advance\d@tmp\dp\@TEXT% + \ifdim\d@hoehe>\d@tmp% + \setbox\@TEXT=\vbox to\d@hoehe{\vfill\box\@TEXT\vspace{.2\baselineskip}\vfill}% + \else% + \setbox\@BILD=\vbox to\d@tmp{\vfill\box\@BILD\vfill}% + \d@hoehe\d@tmp% + \fi% + \fi% + \ifnum\c@piccaption=4% + \make@piccaption% + \d@tmp\ht\@TEXT\advance\d@tmp\dp\@TEXT% + \setbox\@TEXT=\vbox to\d@hoehe{\vspace{-10pt}\box\@TEXT\vfil}% + \advance\d@hoehe-\d@tmp% + \fi% + \ifnum\c@pos=1\d@tmpa=0pt% + \ifnum\c@piccaption>2% + \setbox\@BILD=\hbox{\box\@BILD\hspace{\d@pichskip}\hbox{\box\@TEXT}}% + \fi% + \else\advance\d@tmpa by-\wd\@BILD\d@breite=-\d@breite% + \ifnum\c@piccaption>2% + \d@tmpa=0pt% + \setbox\@BILD=\hbox{\hbox{\box\@TEXT}\hspace{\d@pichskip}\box\@BILD}% + \fi% + \fi% + \p@getot@l\the\pagetotal% + \d@bskip\d@hoehe\advance\d@bskip by\parskip\advance\d@bskip by.3\baselineskip% + {\noindent\hspace*{\d@tmpa}\relax% + \box\@BILD\nopagebreak\vskip-\d@bskip\relax\nopagebreak}% + \d@tmp=-\d@hoehe\divide\d@tmp by\baselineskip% + \c@zeilen=\d@tmp\advance\c@zeilen by-1% + \ifdim\d@breite<0pt\advance\d@breite by-\d@pichskip% + \else\advance\d@breite by\d@pichskip% + \fi% + \hangindent=\d@breite% + \hangafter=\c@zeilen% + \let\par=\x@par% + \ifnum\c@piccaption=3% + \hangindent0pt\hangafter1\let\par=\old@par% + \vskip\d@hoehe\vskip.2\baselineskip% + \fi% + \c@piccaption=0% +} + + + + +\newdimen\ptoti +\newdimen\ptotii +\def\x@par{% + \ptoti\pagetotal% + \old@par% + \ptotii\pagetotal% + \ifdim\ptoti=\ptotii% + \d@tmp\d@hoehe% + \else% + \d@tmp\baselineskip% + \multiply\d@tmp by\prevgraf% + \advance\d@tmp by\parskip% + \global\advance\d@hoehe by-\d@tmp\d@tmp=\d@hoehe% + \fi% + \ifdim\d@hoehe>0pt% + \divide\d@tmp by\baselineskip\c@zeilen=-\d@tmp\advance\c@zeilen by-1% + \c@zeilen=\the\c@zeilen% + \else\c@zeilen=0 + \fi + \ifnum\c@zeilen<0\hangafter=\c@zeilen\hangindent=\d@breite% + \else\let\par=\old@par% + \hangindent 0pt% + \leftskip \d@leftskip% + \if@list\parshape \@ne \@totalleftmargin \linewidth% + \advance\hsize \rightmargin% + \fi% + \fi% +} + + +\def\picskip#1{% + \let\par=\old@par% + \par% + \pagetotal\the\pagetotal% + \c@tmp=#1\relax% + \ifnum\c@tmp=0% + \d@tmp\baselineskip\multiply\d@tmp by\prevgraf\advance\d@tmp\parskip% + \ifdim\p@getot@l<\pagetotal + \advance\d@hoehe by-\d@tmp\advance\d@hoehe by1ex% + \ifdim\d@hoehe>0pt\vspace*{\d@hoehe}\fi% + \fi% + \ifdim\p@getot@l=\pagetotal% + \advance\d@hoehe by-\d@tmp\advance\d@hoehe by1ex% + \ifdim\d@hoehe>0pt\vspace*{\d@hoehe}\fi% + \fi% + \else\hangafter=-\c@tmp\hangindent=\d@breite% + \fi% + \leftskip \d@leftskip% + \if@list\parshape \@ne \@totalleftmargin \linewidth% + \advance\hsize \rightmargin% + \fi% +} + + + + + + +\def\hpic{% + \@ifnextchar ({\ihpic}{\ihpic(0pt,0pt)} +} +\def\ihpic(#1,#2){% + \@ifnextchar ({\@offsettrue\iihpic(#1,#2)}% + {\@offsetfalse\iihpic(#1,#2)(0pt,0pt)} +} +\def\iihpic(#1,#2)(#3,#4){% + \@ifnextchar [{\iiihpic(#1,#2)(#3,#4)}{\iiihpic(#1,#2)(#3,#4)[l]} +} +\def\iiihpic(#1,#2)(#3,#4)[#5]{% + \@ifnextchar [{\ivhpic(#1,#2)(#3,#4)[#5]}{\ivhpic(#1,#2)(#3,#4)[#5][]} +} +\def\ivhpic(#1,#2)(#3,#4)[#5][#6]#7{% + \setbox\@BILD=\hbox{#7}% + \d@breite=#1\d@breite=\the\d@breite% + \ifdim\d@breite=0pt\d@breite=\wd\@BILD\fi% + \c@breite=\d@breite\divide\c@breite by65536% + \d@hoehe=#2\d@hoehe=\the\d@hoehe% + \ifdim\d@hoehe=0pt\d@hoehe=\ht\@BILD\advance\d@hoehe by\dp\@BILD\fi% + \c@hoehe=\d@hoehe\divide\c@hoehe by65536% + \d@xoff=#3\c@xoff=\d@xoff\divide\c@xoff by65536% + \d@yoff=\d@hoehe% + \advance\d@yoff by-#4\c@yoff=\d@yoff\divide\c@yoff by65536% + \c@pos=0\d@tmpa=\parindent\parindent=0pt\unitlength1pt% + \if@offset + \setbox\@BILD=\hbox{% + \begin{picture}(\c@breite,\c@hoehe)% + \put(0,0){\makebox(\c@breite,\c@hoehe){}}% + \put(\c@xoff,\c@yoff){\box\@BILD}% + \end{picture}% + }% + \else% + \setbox\@BILD=\hbox{% + \begin{picture}(\c@breite,\c@hoehe)% + \put(0,0){\makebox(\c@breite,\c@hoehe)[#6]{\box\@BILD}}% + \end{picture}% + }% + \fi% + \@tfor\@tempa := #5\do{% + \if\@tempa f\setbox\@BILD=\hbox{\Rahmen(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa s\setbox\@BILD=\hbox{\Schatten(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa o\setbox\@BILD=\hbox{\Oval(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa d\setbox\@BILD=\hbox{\Strich(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa x\setbox\@BILD=\hbox{\Kasten(\c@breite,\c@hoehe){\box\@BILD}}\fi% + \if\@tempa t\c@pos=1\fi% + \if\@tempa b\c@pos=2\fi% + }% + \ifnum\c@pos=0\parbox{\d@breite}{\makebox[0cm]{}\\\box\@BILD\smallskip}\fi% + \ifnum\c@pos=1\parbox[t]{\d@breite}{\makebox[0cm]{}\\\box\@BILD\smallskip}\fi% + \ifnum\c@pos=2\parbox[b]{\d@breite}{\makebox[0cm]{}\\\box\@BILD\smallskip}\fi% + \parindent=\d@tmpa% +} + + + + + + +\def\Rahmen(#1,#2)#3{% + \c@whole=\@wholewidth\divide\c@whole by65536% + \c@half=\@halfwidth\divide\c@half by65536% + \c@tmpa=#1\advance\c@tmpa by\c@whole\advance\c@tmpa by\c@whole% + \c@tmpb=#2\advance\c@tmpb by\c@whole\advance\c@tmpb by\c@whole% + \begin{picture}(\c@tmpa,\c@tmpb)% + \put(\c@whole,\c@half){\framebox(#1,#2){#3}}% + \end{picture}% + \global\advance\d@breite by2\@wholewidth% + \global\advance\d@hoehe by2\@wholewidth% +} + + +\def\Schatten(#1,#2)#3{% + \c@whole=\@wholewidth\divide\c@whole by65536% + \c@half=\@halfwidth\divide\c@half by65536% + \c@shad=\d@shad\divide\c@shad by65536% + \c@tmp=\c@whole\advance\c@tmp by\c@whole\c@tmpd=\c@tmp% + \advance\c@tmp by\c@shad% + \advance\c@tmpd by#1% + \advance\c@half by\c@shad% + \c@tmpa=#1\advance\c@tmpa by\c@tmp% + \c@tmpb=#2\advance\c@tmpb by\c@tmp% + \begin{picture}(\c@tmpa,\c@tmpb)% + \put(\c@whole,\c@half){\framebox(#1,#2){#3}}% + \put(\c@shad,0){\rule{\c@tmpd pt}{\c@shad pt}}% + \put(\c@tmpd,0){\rule{\c@shad pt}{#2 pt}}% + \end{picture}% + \global\advance\d@breite by2\@wholewidth\global\advance\d@breite by\d@shad% + \global\advance\d@hoehe by2\@wholewidth\global\advance\d@hoehe by\d@shad% +} + + +\def\Oval(#1,#2)#3{% + \@wholewidth=0.4pt% + \c@tmpa=\the#1\divide\c@tmpa by2% + \c@tmpb=\the#2\divide\c@tmpb by2% + \begin{picture}(#1,#2)% + \put(\c@tmpa,\c@tmpb){\oval(#1,#2)}% + \put(0.4,0.4){#3}% + \end{picture}% + \global\advance\d@breite by1pt\global\advance\d@hoehe by1pt% +} + + +\def\Strich(#1,#2)#3{% + \c@whole=\@wholewidth\divide\c@whole by65536% + \c@half=\@halfwidth\divide\c@half by65536% + \c@dash=\d@dash\divide\c@dash by65536% + \c@tmp=\c@whole\advance\c@tmp by\c@whole% + \c@tmpa=#1\advance\c@tmpa by\c@tmp% + \c@tmpb=#2\advance\c@tmpb by\c@tmp% + \c@tmpc=#1\advance\c@tmpc by\c@whole% + \c@tmpd=#2\advance\c@tmpd by\c@whole% + \begin{picture}(\c@tmpa,\c@tmpb)% + \put(\c@half,\c@half){\dashbox{\c@dash}(\c@tmpc,\c@tmpd){#3}}% + \end{picture}% + \global\advance\d@breite by2\@wholewidth% + \global\advance\d@hoehe by2\@wholewidth% +} + + +\def\Kasten(#1,#2)#3{% + \@wholewidth=0.4pt% + \c@boxl=\d@boxl\divide\c@boxl by65536\c@boxl=\the\c@boxl% + \c@tmpa=#1\advance\c@tmpa by\c@boxl% + \c@tmpb=#2\advance\c@tmpb by\c@boxl% + \c@tmp=#2% + \begin{picture}(\c@tmpa,\c@tmpb)% + \put(0,\c@boxl){\framebox(#1,#2){#3}}% + \put(\c@boxl,0){\line(-1,1){\c@boxl}}% + \put(\c@boxl,0){\line(1,0){#1}\line(-1,1){\c@boxl}}% + \put(\c@boxl,0){\put(#1,0){\line(0,1){\c@tmp}% + \put(0,\c@tmp){\line(-1,1){\c@boxl}}}}% + \end{picture}% + \global\advance\d@breite by\d@boxl% + \global\advance\d@hoehe by\d@boxl% +} + + + + + +\newbox\env@box% +\newdimen\d@envdp +\newcount\c@hsize +\newcount\c@envdp +\newdimen\d@envb + +\long\def\frameenv{\@ifnextchar [{\@frameenv}{\@frameenv[\textwidth]}} +\long\def\@frameenv[#1]{% + \hsiz@=\textwidth \textwidth=#1 \d@envb=#1 + \advance\textwidth by-2\@wholewidth + \advance\textwidth by-2\fboxsep + \hsize=\textwidth \linewidth=\textwidth + \setbox\env@box=\vbox\bgroup}% +\def\endframeenv{% + \egroup% + \hsize=\hsiz@ \textwidth=\hsiz@ \linewidth=\hsiz@ + \c@breite=\d@envb \divide\c@breite by65536 + \advance\d@envb by-2\@wholewidth + \c@hsize=\d@envb \divide\c@hsize by65536% + \d@envdp=\dp\env@box \advance\d@envdp by\ht\env@box% + \advance\d@envdp by2\fboxsep% + \d@hoehe=\d@envdp \advance\d@hoehe by2\@wholewidth + \c@hoehe=\d@hoehe \divide\c@hoehe by65536 + \c@envdp=\d@envdp \divide\c@envdp by65536% + \c@tmp=\@wholewidth \divide\c@tmp by65536 + \vskip\@wholewidth% + \unitlength 1pt\noindent% + \begin{picture}(\c@breite,\c@hoehe)(0,0) + \put(\c@tmp,\c@tmp){\framebox(\c@hsize,\c@envdp){\box\env@box}} + \end{picture}% +} + + + +\long\def\shadowenv{\@ifnextchar [{\@shadowenv}{\@shadowenv[\textwidth]}} +\long\def\@shadowenv[#1]{% + \hsiz@=\textwidth \textwidth=#1 \d@envb=#1 + \advance\textwidth by-2\@wholewidth + \advance\textwidth by-2\fboxsep + \advance\textwidth by-\d@shad% + \hsize=\textwidth \linewidth=\textwidth + \setbox\env@box=\vbox\bgroup}% +\def\endshadowenv{% + \egroup + \hsize=\hsiz@ \textwidth=\hsiz@ \linewidth=\hsiz@ + \d@tmpa=\d@envb + \c@breite=\d@envb \divide\c@breite by65536 + \advance\d@envb by-2\@wholewidth \advance\d@envb by-\d@shad + \c@hsize=\d@envb \divide\c@hsize by65536% + \d@envdp=\dp\env@box \advance\d@envdp by\ht\env@box% + \advance\d@envdp by2\fboxsep% + \c@envdp=\d@envdp \divide\c@envdp by65536% + \d@hoehe=\d@envdp + \advance\d@hoehe by2\@wholewidth \advance\d@hoehe by\d@shad + \c@hoehe=\d@hoehe \divide\c@hoehe by65536 + \c@shad =\d@shad \divide\c@shad by65536 + \c@tmp=\@wholewidth \divide\c@tmp by65536 + \advance\d@tmpa by-2\d@shad + \c@xoff =\d@tmpa \divide\c@xoff by65536 + \advance\c@xoff by\c@shad \advance\c@xoff by-1 + \advance\d@envdp by\@wholewidth + \vskip\@halfwidth + \unitlength 1pt\noindent% + \begin{picture}(\c@breite,\c@hoehe)(0,0) + \put(\c@tmp,\c@shad){\framebox(\c@hsize,\c@envdp){\box\env@box}} + \put(\c@shad,0){\rule{\d@tmpa}{\d@shad}}% + \put(\c@xoff,0){\rule{\d@shad}{\d@envdp}}% + \end{picture}% + \vskip\@halfwidth +} + + +\long\def\dashenv{\@ifnextchar [{\@dashenv}{\@dashenv[\textwidth]}} +\long\def\@dashenv[#1]{% + \hsiz@=\textwidth \textwidth=#1 \d@envb=#1 + \advance\textwidth by-2\@wholewidth \advance\textwidth by-2\fboxsep + \hsize=\textwidth \linewidth=\textwidth + \setbox\env@box=\vbox\bgroup}% +\long\def\enddashenv{% + \egroup + \hsize=\hsiz@ \textwidth=\hsiz@ \linewidth=\hsiz@ + \c@breite=\d@envb \divide\c@breite by65536 + \advance\d@envb by-\@wholewidth + \c@hsize=\d@envb \divide\c@hsize by65536% + \d@envdp=\dp\env@box \advance\d@envdp by\ht\env@box% + \advance\d@envdp by2\fboxsep% + \advance\d@envdp by\@wholewidth + \d@hoehe=\d@envdp \advance\d@hoehe by2\@wholewidth + \c@hoehe=\d@hoehe \divide\c@hoehe by65536 + \c@envdp=\d@envdp \divide\c@envdp by65536% + \c@dash=\d@dash \divide\c@dash by65536% + \c@whole=\@wholewidth \divide\c@whole by65536 + \c@half=\@halfwidth \divide\c@half by 65536 + \noindent\unitlength 1pt + \begin{picture}(\c@breite,\c@hoehe)(0,0) + \put(\c@half,\c@whole){\dashbox{\c@dash}(\c@hsize,\c@envdp){\box\env@box}} + \end{picture}% +} + + +\long\def\ovalenv{\@ifnextchar [{\@ovalenv}{\@ovalenv[\textwidth]}}% +\long\def\@ovalenv[#1]{% + \hsiz@=\textwidth \textwidth=#1 \d@envb=#1 + \advance\textwidth by-4\fboxsep + \hsize=\textwidth \linewidth=\textwidth + \setbox\env@box=\vbox\bgroup}% +\long\def\endovalenv{% + \egroup + \hsize=\hsiz@ \textwidth=\hsiz@ \linewidth=\hsiz@ + \@wholewidth=0.4pt + \c@breite=\d@envb \divide\c@breite by65536 + \advance\d@envb by-2\@wholewidth + \c@hsize=\d@envb \divide\c@hsize by65536% + \d@envdp=\dp\env@box \advance\d@envdp by\ht\env@box% + \advance\d@envdp by4\fboxsep% + \c@envdp=\d@envdp \divide\c@envdp by65536% + \d@hoehe=\d@envdp \advance\d@hoehe by2\@wholewidth + \c@hoehe=\d@hoehe \divide\c@hoehe by65536 + \c@tmpa=\c@hsize \divide\c@tmpa by2% + \c@tmpb=\c@envdp \divide\c@tmpb by2% + \d@tmpa=2\fboxsep \advance\d@tmpa by\@wholewidth + \c@xoff=\d@tmpa \divide\c@xoff by65536% + \advance\d@tmpa by\dp\env@box + \c@yoff=\d@tmpa \divide\c@yoff by65536% + \unitlength 1pt\noindent + \begin{picture}(\c@breite,\c@hoehe)(0,0) + \put(\c@tmpa,\c@tmpb){\oval(\c@hsize,\c@envdp)} + \put(\c@xoff,\c@yoff){\box\env@box}% + \end{picture}% +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/reference.bib Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,33 @@ +@Misc{Yasutaka:2016, + author = "{比嘉 健太, 河野 真治}", + title = "{メタ計算を用いた Continuation based C の検証手法}", + journal = "琉球大学工学部情報工学科平成 28 年度学位論文", + year = 2016 +} + +@Misc{Tatsuki:2016, + author = "{伊波 立樹, 東恩納 琢偉, 河野 真治}", + title = "{Code Gear 、Data Gear に基づく OS のプロトタイプ}", + journal = "{情報処理学会システムソフトウェアとオペレーティングシステム研究会}", + year = 2016 +} + +@Misc{kaito:2015, + author = "{徳森 海斗, 河野 真治}", + title = "{LLVM Clang 上の Continuation based C コンパイラ の改良}", + journal = "{琉球大学工学部情報工学科平成 27 年度学位論文}", + year = 2015 +} + +@misc{agda, + title = {The Agda wiki}, + howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, + note = {Accessed: 2017/10/24(Tue)} +} + + +@misc{agda-documentation, + title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation}, + howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}}, + note = {Accessed: 2017/10/24(Tue)} +} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/SingleLinkedStack.cbc Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,32 @@ +__code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} +__code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} + +__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + if (stack->top) { + data1 = stack->top->data; + stack->top = stack->top->next; + } else { + data1 = NULL; + } + goto next(data, data1, ...); +} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/SingleLinkedStack.cbc.replace Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,16 @@ +__code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} +__code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/push-pop.cbc Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,32 @@ + __code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} + __code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} + +__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + if (stack->top) { + data1 = stack->top->data; + stack->top = stack->top->next; + } else { + data1 = NULL; + } + goto next(data, data1, ...); +} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/stack.agda.replace Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,12 @@ +record Stack {a t : Set} (stackImpl : Set) : Set where +field +stack : stackImpl +push : stackImpl -> a -> (stackImpl -> t) -> t +pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t +open Stack + +pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t +pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) + +popStack : {a t : Set} -> Stack a -> (Stack t -> t) -> t +popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/stack_context.h.replace Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,14 @@ +struct Stack { + union Data* stack; + union Data* data; + union Data* data1; + enum Code whenEmpty; + enum Code clear; + enum Code push; + enum Code pop; + enum Code pop2; + enum Code isEmpty; + enum Code get; + enum Code get2; + enum Code next; +} Stack;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/pic/emblem-bitmap.xbb Thu Nov 08 10:57:19 2018 +0900 @@ -0,0 +1,8 @@ +%%Title: emblem-bitmap.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 451 246 +%%HiResBoundingBox: 0.000000 0.000000 451.000000 246.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Thu Oct 26 13:59:32 2017 +