--- a/Paper/master_paper.tex	Fri Jan 20 15:20:31 2023 +0900
+++ b/Paper/master_paper.tex	Sat Jan 21 17:57:20 2023 +0900
@@ -18,21 +18,19 @@
 %\input{dummy.tex} %% font
 
 \jtitle{Gears Agda での形式手法}
-\etitle{} %
+\etitle{Formal Methods in Gears Agda} %
 \year{2023年 3月}
-\eyear{March 2022}
+\eyear{March 2023}
 \author{上地 悠斗}
 \eauthor{Yuto Uechi}
 \chife{指導教員：教授 和田 知久}
 \echife{Supervisor: Prof. Tomohisa Wada}
 
-
 \marklefthead{% 左上に挿入
   \begin{minipage}[b]{.4\textwidth}
     琉球大学大学院学位論文(修士)
 \end{minipage}}
 
-
 % \markleftfoot{% 左下に挿入
 %  \begin{minipage}{.8\textwidth}
 %    Gears OS の Paging
@@ -85,11 +83,11 @@
 \begin{document}
 %rome
 \maketitle
-
+\pagenumbering{roman}
+\setcounter{page}{0}
 \newpage
 
-\pagenumbering{roman}
-\setcounter{page}{0}
+
 \makecommission
 %\input{chapter/signature.tex}
 
@@ -142,6 +140,8 @@
 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
 \section{Gears Agdaによるモデル検査の流れ}
 
+% Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い
+
 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
 \chapter{今後の展望}