--- a/Paper/master_paper.tex	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/master_paper.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -137,14 +137,14 @@
 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
 そのため、並列処理はモデル検査にて検証する。
 \section{モデル検査とは}
-\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
+\input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
 \section{Gears Agdaによるモデル検査の流れ}
 
 % Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い
 
 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
-\chapter{今後の展望}
+\chapter{まとめと今後の展望}
 ここまでで Gears Agda により定理証明を用いた検証と
 モデル検査による検証方法を確立した．
 これからは Red Black Tree の定理証明を用いた検証と，