Mercurial > hg > Papers > 2017 > atton-master
annotate paper/atton-master.tex @ 35:26c89a10de3c
Update TODO
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 28 Jan 2017 09:47:44 +0900 |
parents | 9800586284e1 |
children | d14c3fa5f3ea |
rev | line source |
---|---|
35 | 1 % TODO lists |
29 | 2 % 比較対象 |
3 % agda の stack? | |
4 % akasha は別 chapter にして | |
5 % あと syntax を最新に合わせて動かしてくれ | |
6 % type system に名前を付ける? | |
7 % 先の展望を書くべきだな | |
35 | 8 % gears and monad |
9 % delta monad | |
10 % 副査名修正 | |
11 | |
29 | 12 |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 \documentclass[a4j,12pt]{jreport} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 \usepackage{master_paper} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 \usepackage{ascmac} |
34 | 16 \usepackage{bussproofs} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 \usepackage[dvipdfmx]{graphicx} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 \usepackage{here} |
3 | 19 \usepackage{listings} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 \usepackage{comment} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 \usepackage[deluxe, multi]{otf} |
5
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
22 \usepackage{url} |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
23 \usepackage{cite} |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
24 \usepackage{listings} |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
25 \usepackage{bussproofs} |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
26 \usepackage{amssymb} |
10 | 27 \usepackage{amsmath} |
5
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
28 \usepackage[utf8]{inputenc} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 %\input{dummy.tex} %% font |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
4 | 32 \jtitle{メタ計算を用いた Continuation based C の検証手法} |
33 \etitle{Verification Methods of Continuation based C using Meta Computations} | |
3 | 34 \year{2017年 3月} |
35 \eyear{March 2017} | |
4 | 36 \author{比嘉 健太} |
37 \eauthor{Yasutaka HIGA} | |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 \chife{指導教員:教授 和田 知久} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 \echife{Supervisor: Prof. Tomohisa WADA} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 \marklefthead{% 左上に挿入 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 \begin{minipage}[b]{.4\textwidth} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 琉球大学大学院学位論文(修士) |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 \end{minipage}} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 \markleftfoot{% 左下に挿入 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 \begin{minipage}{.8\textwidth} |
4 | 48 メタ計算を用いた Continuation based C の検証手法 |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 \end{minipage}} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 \newcommand\figref[1]{図 \ref{fig:#1}} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 \newcommand\tabref[1]{表 \ref{tab:#1}} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 \lstset{ |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 frame=single, |
5
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
56 keepspaces=true, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
57 stringstyle={\ttfamily}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
58 commentstyle={\ttfamily}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
59 identifierstyle={\ttfamily}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
60 keywordstyle={\ttfamily}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
61 basicstyle={\ttfamily}, |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 breaklines=true, |
5
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
63 xleftmargin=0zw, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
64 xrightmargin=0zw, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
65 framerule=.2pt, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
66 columns=[l]{fullflexible}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
67 numbers=left, |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 stepnumber=1, |
5
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
69 numberstyle={\scriptsize}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
70 numbersep=1em, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
71 language={}, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
72 tabsize=4, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
73 lineskip=-0.5zw, |
cb4bf01e9ad9
Add packages from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
74 escapechar={@}, |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 } |
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
76 \def\lstlistingname{リスト} |
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
77 \def\lstlistlistingname{リスト目次} |
34 | 78 \newtheorem{defi}{定義}[section] |
79 | |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 %%% 索引のために以下の2行を追加 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 \usepackage{makeidx,multicol} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 \makeindex |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 \begin{document} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 %rome |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 \frontmatter |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 \maketitle |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 \newpage |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 \makecommission |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 %要旨 |
10 | 95 \input{abstract.tex} |
96 \input{abstract_eng.tex} | |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 %目次 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 \tableofcontents |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 %図目次 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 \listoffigures |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 %表目次 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 \listoftables |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 |
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
107 %リスト目次 |
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
108 \lstlistoflistings |
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
109 |
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
110 |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 %arabic |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 \mainmatter |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 %chapters |
20 | 115 \input{introduction.tex} |
9
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
116 |
12 | 117 \input{cbc.tex} |
28 | 118 \input{type.tex} |
9
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
119 |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
120 \chapter{証明支援系言語 Agda による証明手法} |
22 | 121 \label{chapter:agda} |
10 | 122 \section{依存型を持つ証明支援系言語 Agda} |
9
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
123 \section{Natural Deduction} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
124 \section{Curry-Howard Isomorphism} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
125 \section{Reasoning} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
126 |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
127 \chapter{Agda における Continuation based C の表現} |
22 | 128 \label{chapter:subtype} |
9
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
129 \section{CodeSegment の定義} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
130 \section{DataSegment の定義} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
131 \section{ノーマルレベル計算の実行} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
132 \section{MetaCodeSegment の定義} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
133 \section{MetaDataSegment の定義} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
134 \section{メタレベル計算の実行} |
11 | 135 \section{Agda を用いたContinuation based C の検証} |
9
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
136 \section{スタックの実装の検証} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
137 |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
138 \chapter{まとめ} |
f6931d3d59c0
Add first table of contents
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
139 \section{今後の課題} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
140 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
141 %謝辞 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
142 \addcontentsline{toc}{chapter}{謝辞} |
7 | 143 \input{thanks.tex} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 %参考文献 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 \nocite{*} |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 \bibliographystyle{junsrt} |
6
5c0e43b1b559
Import reference from atton-thesis
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
5
diff
changeset
|
148 \bibliography{reference} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
149 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
150 %発表履歴 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
151 \addcontentsline{toc}{chapter}{発表履歴} |
8 | 152 \input{history.tex} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
153 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
154 %付録 |
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
155 \addcontentsline{toc}{chapter}{付録} |
3 | 156 % \input{appendix.tex} |
2
a8d3cbdebb3e
Import main tex file from kkb-master
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
157 \end{document} |