# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424007523 -32400
# Node ID ca389989b660252737a831d75154a580c1c59ce2
# Parent  6ca594d19ca4e24cc6a9844b64976672f6cea850
Add original sources

diff -r 6ca594d19ca4 -r ca389989b660 main.tex
--- a/main.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/main.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -3,6 +3,7 @@
 \usepackage{mythesis}
 \usepackage{multirow}
 \usepackage{here}
+\usepackage{float}
 \usepackage{listings}
 \usepackage{bussproofs}
 \usepackage{amssymb}
@@ -92,8 +93,7 @@
 
 % 付録
 \appendix
+\input{original_sources}
 % \input{proof_deltaM}
-% TODO: 実験環境
-% TODO: Delta と DeltaM の本体
 
 \end{document}
diff -r 6ca594d19ca4 -r ca389989b660 original_sources.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/original_sources.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,38 @@
+\chapter{Haskell による Delta と DeltaM の定義と使用例のプログラム}
+\label{chapter:original_sources}
+
+\section{実験環境}
+
+表\ref{table:environment}に実験環境におけるプログラムやライブラリのバージョンを示す。
+
+\begin{table}[htbp]
+    \begin{center}
+        \begin{tabular}{|c||c|} \hline
+            & version   \\ \hline \hline
+            Mac OS X & 10.9.5    \\ \hline
+            ghc      & 7.8.4     \\ \hline
+            Agda     & 2.4.2.2   \\ \hline
+            cabal    & 1.22.0.0  \\ \hline
+        \end{tabular}
+        \label{table:environment}
+        \caption{実験環境}
+    \end{center}
+\end{table}
+
+\section{Delta と DeltaM のソースコード}
+
+\begin{table}[html]
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:original_delta,
+                     caption= Delta のソースコード,
+                     escapechar=&] {src/orig/Delta.hs}
+\end{table}
+
+\begin{table}[html]
+    \lstinputlisting[basicstyle={\scriptsize},
+                     numberstyle={\tiny},
+                     label=src:original_deltaM,
+                     caption= DeltaM のソースコード,
+                     escapechar=&] {src/orig/DeltaM.hs}
+\end{table}
diff -r 6ca594d19ca4 -r ca389989b660 proof_deltaM.tex
--- a/proof_deltaM.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/proof_deltaM.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -1,2 +1,20 @@
 \section{DeltaM が Monad 則を満たす証明}
+DeltaM に対する Monad 則の証明も Agda によって行なう。
+プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 
+内部に持つ型引数を持つ型M は Functor と Monad であるとする。
+基本的に同じ法則を用いて証明していくことになる。
+例えば $ \eta $ が natural transformation である証明には、 M の $ \eta $ が natural transformation である証明を用いる。
+また、同じ値に対して同じ振舞いをする関数を fmap しても同じであるという fmap-equiv という等式を導入している。
+これは高階関数に対する等式が定義できなかったためである。
+
+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}
diff -r 6ca594d19ca4 -r ca389989b660 src/deltaM_is_monad.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/deltaM_is_monad.agda	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,443 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+open import basic
+open import delta
+open import delta.functor
+open import delta.monad
+open import deltaM
+open import deltaM.functor
+open import nat
+open import laws
+
+module deltaM.monad where
+open Functor
+open NaturalTransformation
+open Monad
+
+
+-- sub proofs
+
+deconstruct-id : {l : Level} {A : Set l} {n : Nat}
+                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d
+deconstruct-id {n = O}   (deltaM x) = refl
+deconstruct-id {n = S n} (deltaM x) = refl
+
+headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (x : (DeltaM M A (S n))) ->
+                    ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
+headDeltaM-with-f {n = O} f   (deltaM (mono x))    = refl
+headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
+
+
+tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
+                    (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
+tailDeltaM-with-f {n = O} f (deltaM (delta x d))   = refl
+tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
+
+
+
+fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
+                                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                                 (x : T (DeltaM M (DeltaM M A (S n)) (S n))) ->
+                   fmap F (headDeltaM ∙ deltaM-mu) x ≡ fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x
+fmap-headDeltaM-with-deltaM-mu {n = O}   x = refl
+fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl
+
+
+fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
+                                 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+               (d : DeltaM M (DeltaM M (DeltaM M A (S (S n))) (S (S n))) (S n)) ->
+                deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d
+fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
+fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d)      = refl
+
+
+
+
+
+-- main proofs
+
+deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                   {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                   (f : A -> B) -> (x : A) ->
+                   ((deltaM-eta {l} {B} {n} {T} {F} {M} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
+deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x   = begin
+  deltaM-eta {n = O} (f x)              ≡⟨ refl ⟩
+  deltaM (mono (eta mm (f x)))          ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
+  deltaM (mono (fmap fm f (eta mm x)))  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM-eta {n = O} x)  ∎
+deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin
+  deltaM-eta {n = S n} (f x)
+  ≡⟨ refl ⟩
+  deltaM (delta-eta {n = S n} (eta mm (f x)))
+  ≡⟨ refl ⟩
+  deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x))))
+  ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩
+  deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x))))
+  ≡⟨ cong (\de ->  deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
+  deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM-eta {n = S n} x)
+  ∎
+
+
+
+
+deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                  (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
+                  deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
+deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M}  f (deltaM (mono x)) = begin
+  deltaM-fmap f (deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
+  ∎
+deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin
+  deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d)))))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta de
+                  (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (mu-is-nt M f (fmap F headDeltaM x)))  ⟩
+  deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (fmap-equiv F (headDeltaM-with-f f) x)  ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
+           (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d)))))
+
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+               (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))))
+           (covariant F (deltaM-fmap f) headDeltaM x) ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
+  ∎
+
+
+
+
+
+deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
+                         {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                         (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
+deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
+  deltaM-mu (deltaM-eta (deltaM (mono x)))             ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
+  deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
+  deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
+  deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
+  deltaM (mono x)
+  ∎
+deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-eta (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta {l} {T (DeltaM M A (S (S n)))} {n} (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d)))))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (eta M (deltaM (delta x d)))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
+     (sym (eta-is-nt M headDeltaM (deltaM (delta x d)))) ⟩
+  deltaM (delta (mu M (eta M (headDeltaM {M = M} (deltaM (delta x d)))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (eta M x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
+           (sym (right-unity-law M x)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
+           (sym (delta-eta-is-nt (fmap F tailDeltaM)  (eta M (deltaM (delta x d))))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (fmap F tailDeltaM (eta M (deltaM (delta x d)))))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta de))))))
+           (sym (eta-is-nt M tailDeltaM (deltaM (delta x d)))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (tailDeltaM (deltaM (delta x d)))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d)))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM d)))
+  ≡⟨ refl ⟩
+  deltaM (delta x d)
+  ∎
+
+
+
+
+
+
+deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
+                        {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                        (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
+deltaM-left-unity-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = begin
+  deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-eta x)))      ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x)))))))      ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (eta M) x)))
+  ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
+  deltaM (mono x)
+  ∎
+deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))
+  (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (fmap F deltaM-eta x)))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
+           (sym (covariant F deltaM-eta headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {n = S n} {M = M}) ∙  deltaM-eta) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (eta M) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
+           (left-unity-law M x) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
+  deltaM (delta x (unDeltaM {M = M} (deltaM d)))
+  ≡⟨ refl ⟩
+  deltaM (delta x d)
+  ∎
+
+deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
+                         {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                         (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n))  (S n)) ->
+                         deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
+deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x))    = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-mu x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x)))))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x)))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (mono x)))
+
+  ∎
+
+deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))))))))
+
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {A = A} {M = M}) (fmap F deltaM-mu x)))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))))
+           (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {A = A} {M = M}) ∙  deltaM-mu) x))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                          (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d)))))))
+           (fmap-headDeltaM-with-deltaM-mu {A = A} {M = M} x) ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {A = A} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-mu) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-covariant tailDeltaM deltaM-mu (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (fmap-tailDeltaM-with-deltaM-mu (deltaM d))  ⟩
+  deltaM (delta (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                          (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+          (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) ∙ (fmap F headDeltaM)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (((fmap F ((mu M) ∙ (fmap F headDeltaM))) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de)
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (covariant F (fmap F headDeltaM)  (mu M) (fmap F headDeltaM x)) ⟩
+
+  deltaM (delta (mu M ((((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (mu M) (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (delta (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
+           (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
+  ≡⟨ cong (\de ->   deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM))  ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))  ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x)))) (unDeltaM {M = M} de)))
+           (deltaM-association-law (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
+
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                                 (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                                 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
+           (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (mu M (fmap F headDeltaM x))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM
+                  (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
+
+
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} ((deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
+
+
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM x))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d)))))
+                           (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (delta x d)))
+  ∎
+
+
+
+
+deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
+                  Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n})
+deltaM-is-monad {l} {A} {n} {T} {F} {M} =
+                record { mu     = deltaM-mu
+                       ; eta    = deltaM-eta
+                       ; eta-is-nt = deltaM-eta-is-nt
+                       ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
+                       ; association-law = deltaM-association-law
+                       ; left-unity-law  = deltaM-left-unity-law
+                       ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
+                       }
diff -r 6ca594d19ca4 -r ca389989b660 src/orig/Delta.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Delta.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,56 @@
+module Delta ( Delta(..) , deltaAppend , headDelta , tailDelta , deltaFromList) where
+
+import Control.Applicative
+
+
+-- Delta definition
+
+data Delta a = Mono a | Delta a (Delta a) deriving Show
+
+instance (Eq a) => Eq (Delta a) where
+    (Mono x) == (Mono y)         = x == y
+    (Mono _) == (Delta _ _)      = False
+    (Delta x xs) == (Delta y ys) = (x == y) && (xs == ys)
+
+-- basic functions
+
+deltaAppend :: Delta a -> Delta a -> Delta a
+deltaAppend (Mono x) d     = Delta x d
+deltaAppend (Delta x d) ds = Delta x (deltaAppend d ds)
+
+headDelta :: Delta a -> a
+headDelta (Mono  x)   = x
+headDelta (Delta x _) = x
+
+tailDelta :: Delta a -> Delta a
+tailDelta d@(Mono _)   = d
+tailDelta (Delta _ ds) = ds
+
+-- instance definitions
+
+instance Functor Delta where
+    fmap f (Mono x)    = Mono  (f x)
+    fmap f (Delta x d) = Delta (f x) (fmap f d)
+
+instance Applicative Delta where
+    pure f                       = Mono  f
+    (Mono f)     <*> (Mono x)    = Mono  (f x)
+    df@(Mono f)  <*> (Delta x d) = Delta (f x) (df <*> d)
+    (Delta f df) <*> d@(Mono x)  = Delta (f x) (df <*> d)
+    (Delta f df) <*> (Delta x d) = Delta (f x) (df <*> d)
+
+bind :: (Delta a) -> (a -> Delta b) -> (Delta b)
+bind (Mono x)    f = f x
+bind (Delta x d) f = Delta (headDelta (f x)) (bind d (tailDelta . f))
+
+mu :: (Delta (Delta a)) -> (Delta a)
+mu d = bind d id
+
+instance Monad Delta where
+    return x = Mono x
+    d >>= f  = mu $ fmap f d
+
+-- utils
+
+deltaFromList :: [a] -> Delta a
+deltaFromList = (foldl1 deltaAppend) . (fmap return)
diff -r 6ca594d19ca4 -r ca389989b660 src/orig/DeltaM.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/DeltaM.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,56 @@
+module DeltaM (DeltaM(..), unDeltaM, appendDeltaM, tailDeltaM, headDeltaM, checkOut) where
+
+import Control.Applicative
+import Delta
+
+
+-- DeltaM definition (Delta with Monad)
+
+data DeltaM m a = DeltaM (Delta (m a)) deriving (Show)
+
+
+-- DeltaM utils
+
+unDeltaM :: DeltaM m a -> Delta (m a)
+unDeltaM (DeltaM d) = d
+
+headDeltaM :: DeltaM m a -> m a
+headDeltaM (DeltaM d) = headDelta d
+
+tailDeltaM :: DeltaM m a -> DeltaM m a
+tailDeltaM (DeltaM d) = DeltaM $ tailDelta d
+
+appendDeltaM :: DeltaM m a -> DeltaM m a -> DeltaM m a
+appendDeltaM (DeltaM d) (DeltaM dd) = DeltaM (deltaAppend d dd)
+
+checkOut :: Int -> DeltaM m a -> m a
+checkOut 0 (DeltaM (Mono x))    = x
+checkOut 0 (DeltaM (Delta x _)) = x
+checkOut n (DeltaM (Mono x))    = x
+checkOut n (DeltaM (Delta _ d)) = checkOut (n-1) (DeltaM d)
+
+
+-- DeltaM instance definitions
+
+instance (Functor m) => Functor (DeltaM m) where
+    fmap f (DeltaM d) = DeltaM $ fmap (fmap f) d
+
+instance (Applicative m) => Applicative (DeltaM m) where
+    pure f                                          = DeltaM $ Mono $ pure f
+    (DeltaM (Mono f))     <*> (DeltaM (Mono x))     = DeltaM $ Mono $ f <*> x
+    df@(DeltaM (Mono f))  <*> (DeltaM (Delta x d))  = appendDeltaM (DeltaM $ Mono $ f <*> x) (df <*> (DeltaM d))
+    (DeltaM (Delta f df)) <*> dx@(DeltaM (Mono x))  = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> dx)
+    (DeltaM (Delta f df)) <*> (DeltaM (Delta x dx)) = appendDeltaM (DeltaM $ Mono $ f <*> x) ((DeltaM df) <*> (DeltaM dx))
+
+
+mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a
+mu' d@(DeltaM (Mono _))    = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d
+mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d)
+                                            (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d))))
+
+instance (Functor m, Monad m) => Monad (DeltaM m) where
+    return x = DeltaM $ Mono $ return x
+    d >>= f  = mu' $ fmap f d
+
+
+
diff -r 6ca594d19ca4 -r ca389989b660 src/orig/Example/Delta.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Example/Delta.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,22 @@
+module Example.Delta where
+
+import Data.Numbers.Primes
+import Delta
+
+-- examples
+
+generator :: Int -> Delta [Int]
+generator x = let intList = [1..x] in
+                  return intList
+
+numberFilter :: [Int] -> Delta [Int]
+numberFilter xs = let primeList = filter isPrime xs
+                      evenList  = filter even xs    in
+                  Delta evenList (Mono primeList)
+
+count :: [Int] -> Delta Int
+count xs = let primeCount = length xs in
+           return primeCount
+
+numberCount :: Int -> Delta Int
+numberCount x = generator x >>= numberFilter >>= count
diff -r 6ca594d19ca4 -r ca389989b660 src/orig/Example/DeltaM.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/orig/Example/DeltaM.hs	Sun Feb 15 22:38:43 2015 +0900
@@ -0,0 +1,46 @@
+module Example.DeltaM where
+
+import Control.Monad.Writer
+import Data.Numbers.Primes -- $ cabal install primes
+
+import Delta
+import DeltaM
+
+
+-- DeltaM examples
+
+-- DeltaM example utils
+type DeltaLog     = Writer [String]
+type DeltaWithLog = DeltaM DeltaLog
+
+returnW :: (Show a) => a -> DeltaLog a
+returnW x = do tell $ [show x]
+               return x
+
+dmap :: (m a -> b) -> DeltaM m a -> Delta b
+dmap f (DeltaM d) = fmap f d
+
+deltaWithLogFromList :: (Show a) => [a] -> DeltaWithLog a
+deltaWithLogFromList xs = DeltaM $ deltaFromList $ fmap returnW xs
+
+
+-- example : prime filter
+-- usage   : runWriter $ checkOut 0 $ numberCountM 30  -- run specific version
+--         : dmap runWriter $ numberCountM 30          -- run all version
+
+generatorM :: Int -> DeltaWithLog [Int]
+generatorM x = let intList = [1..x] in
+                             DeltaM $ deltaFromList $ fmap returnW $ replicate 2 intList
+
+numberFilterM :: [Int] -> DeltaWithLog [Int]
+numberFilterM xs = let primeList = filter isPrime xs
+                       evenList  = filter even xs    in
+                      DeltaM $ deltaFromList $ fmap returnW [primeList, evenList]
+
+
+countM :: [Int] -> DeltaWithLog Int
+countM xs = let numberCount = length xs in
+                DeltaM $ deltaFromList $ fmap returnW $ replicate 2 numberCount
+
+numberCountM :: Int -> DeltaWithLog Int
+numberCountM x = generatorM x >>= numberFilterM >>= countM
diff -r 6ca594d19ca4 -r ca389989b660 thanks.tex
--- a/thanks.tex	Sun Feb 15 21:56:19 2015 +0900
+++ b/thanks.tex	Sun Feb 15 22:38:43 2015 +0900
@@ -6,7 +6,7 @@
 %GISゼミや英語ゼミに参加した人はその分も入れておく．
 %順番は重要なので気を付けるように．(提出前に周りの人に確認してもらう．)
 
-\hspace{1zw}本研究の遂行、また本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治準教授に深く感謝したします。
+\hspace{1zw}本研究の遂行、また本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に深く感謝致します。
 
 また一年間共に研究を行い、暖かな気遣いと励ましをもって支えてくれた並列信頼研究室のみなさんに感謝致します。