# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424062070 -32400
# Node ID 43213dcf8d24642d48d259af19d2cafac2f76a9c
# Parent  bf136bd59e7a929c7d15d81a3b8e5249008c4a44
Add proof DeltaM

diff -r bf136bd59e7a -r 43213dcf8d24 delta_with_monad.tex
--- a/delta_with_monad.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/delta_with_monad.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -136,7 +136,7 @@
 
 このように、Monad と組み合せることでトレースを得ることができた。
 Writer 以外にも任意の Monad に対して DeltaM が Monad 則を満たす。
-この証明は非常に長いので付録に載せるものとする。% TODO ref
+この証明は非常に長いので付録\ref{section:proof_deltaM}に載せるものとする。
 
 DeltaM を定義した結果、Delta Monadと Monad を組み合せることができた。
 
diff -r bf136bd59e7a -r 43213dcf8d24 main.tex
--- a/main.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/main.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -94,6 +94,6 @@
 % 付録
 \appendix
 \input{original_sources}
-% \input{proof_deltaM}
+\input{proof_deltaM}
 
 \end{document}
diff -r bf136bd59e7a -r 43213dcf8d24 proof_deltaM.tex
--- a/proof_deltaM.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/proof_deltaM.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -1,4 +1,5 @@
-\section{DeltaM が Monad 則を満たす証明}
+\chapter{DeltaM が Monad 則を満たす証明}
+\label{section:proof_deltaM}
 DeltaM に対する Monad 則の証明も Agda によって行なう。
 プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 
@@ -11,10 +12,10 @@
 DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
 なお、Functor則に対する証明も行なったが省略する。
 
-\begin{table}
-    \lstinputlisting[basicstyle={\scriptsize},
-                     numberstyle={\tiny},
-                     label=src:deltaM_is_monad,
-                     caption= DeltaM が Monad 則を満たす証明]
-                     {src/deltaM_is_monad.agda.replaced}
-\end{table}
+
+\lstinputlisting[basicstyle={\scriptsize},
+                 numberstyle={\tiny},
+                 label=src:deltaM_is_monad,
+                 caption= DeltaM が Monad 則を満たす証明]
+                 {src/deltaM_is_monad.agda.replaced}
+