--- a/final_main/chapter2.tex	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/chapter2.tex	Sun Feb 18 21:43:41 2018 +0900
@@ -40,7 +40,6 @@
 % \label{sec:withEnv}
 % 環境付き継続の話はいらないよね
 
-
 \section{CbC での CodeGear と DataGear } %% 例題
 %% Metaな話は今書いてもどうせ使わないので検証に使える〜くらいで置いておく？
 %% 部分は生成でき、そこで検証用の動作をする感じでは？hora理論使ったりするといい
@@ -128,6 +127,7 @@
 \end{figure}
 
 
+
 \section{メタ計算}
 % メタ計算の論文引用どうするかな…
 % メタプログラミング~系の本とかもいれていいのかな
@@ -139,6 +139,8 @@
 と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管
 理やスレッド管理、資源管理等の計算がこれに当たる。
 
+
+
 % \section{Meta CodeGear とMeta DataGear}
 
 % CbC 
@@ -157,12 +159,32 @@
 
 % Interface を記述することでデータ構造の api と DataGear の結びつきを高め、呼び出しが容易になる。
 
+
+\section{Context}
+CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ
+スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。
+CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必
+要がある。
+
+\section{stub CodeGear}
+CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。
+しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では
+Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear
+を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス
+することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接
+続される。
+stub CodeGear は CodeGear の Meta CodeGear に当たる。
+
+
 \section{CbCによる Interface の記述と継続}
 
 CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき
 る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear
 、 Meta DataGear が存在する。
 
+CbC で実装していると、stub CodeGear の記述が煩雑になることが分かった。
+そのため 既存の実装を モジュールとして扱うため Interface という仕組みを導入した。
+
 DataGear に対して何らかの操作(API)を行う CodeGear とその
 CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
 として定義される。

--- a/final_main/chapter3.tex	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/chapter3.tex	Sun Feb 18 21:43:41 2018 +0900
@@ -215,13 +215,13 @@
 
 \begin{eqnarray}
     \label{exp:a_implies_b}
-    B \\ \nonumber
+    A \\ \nonumber
     \vdots \\ \nonumber
-    A \\ \nonumber
+    B \\ \nonumber
 \end{eqnarray}
 
-式\ref{exp:a_implies_b}のように B を仮定して A を導いたとする。
-この時 B は alive な仮定であり、証明された A は B の仮定に依存していることを意味する。
+式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
+この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
 
 ここで、推論規則により記号 $ \Rightarrow $ を導入する。
 

--- a/final_main/chapter4.tex	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/chapter4.tex	Sun Feb 18 21:43:41 2018 +0900
@@ -10,9 +10,10 @@
 % どうするのかは書けるけどなんでAgdaなの？みたいな話が飛んでくる
 
 前章では Agda の文法について説明した。
-本章では CbC 
+本章では CbC と対応して CodeGear、 DataGear、 継続を Agda で表現する。
+また、 Agda で継続を記述することで得た知見を示す。
 
-\section{Agda での CodeGear と DataGear の表現}
+\section{Agda での CodeGear 、 DataGear 、 継続の表現}
 
 %% 書くこと
 % CodeGearとDataGearのAgda上での定義
@@ -24,20 +25,43 @@
 \lstinputlisting[label=src:agda-ds, caption=Agda における DataGear の定義]
 {src/DataSegment.agda.replaced}
 
-
 CodeGear は DataGear を受け取って DataGear を返すという定義であるため、
 $ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{src:agda-cs})を定義する。
 
 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced}
 
-この CodeGear 型の定義により、 Agda での CodeGear の本体は Agda での関数そのものとして扱う。
+CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの
+と対応する。
 % しかし、そのままだと再帰呼び出しの点で CbC との対応が失われてしまう。
 % そのため、 Agda では \verb/goto/を利用できるのは関数の末尾のみという制約を設ける
 % 必要がある。
+% この制約さえ満たせば、
 
-% この制約さえ満たせば、
-CodeGear の実行は CodeGear 型から関数本体を取り出し、
-レコード型を持つ値を適用することに相当する。
+CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す
+ることに相当する。
+
+
+CbC での軽量継続は
+
+\begin{itemize}
+ \item 次に実行する CodeGear を指定する
+ \item CodeGear に渡す DataGear を指定する
+ \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
+\end{itemize}
+
+の機能を持っている。
+
+この機能を満たす関数はソースコード\ref{src:agda-goto} として定義されている。
+
+\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced}
+
+goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
+CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。
+
+
+\section{Agda での Stack、 Tree の実装}
+
+
 
 \section{Agda における Interface の実装}
 
@@ -46,12 +70,19 @@
 % interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい
 
 Agda 側でも CbC 側と同様に interface を実装した。
-ここでは Stack の interface を例に取る。
-interface は record で列挙し、~\ref{src:agda-interface}のように紐付けることができる。
-CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を書いている。
+interface は record で列挙し、ソースコード~\ref{src:agda-interface}のように紐付けることができる。
+CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。
+
+例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。
+Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から
+interface を通して呼び出している。
 
-例として Agda で実装した Stack 上のinterface を見る。
-ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 実際に使われる Stack の操作は StackMethods にある push や popである。
+ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
+実際に使われる Stack の操作は StackMethods にある push や popである。この push
+や pop は SingleLinkedStack で実装されている。
+
+\lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack
+の実装] {src/AgdaSingleLinkedStack.agda.replaced}
 
 \lstinputlisting[label=src:agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda.replaced}
 
@@ -59,18 +90,22 @@
 り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
 して継続を返す型に変わっている。
 
-interface を記述することによって、データを push する際に予め決まっている引数を減
-らすことができた。
+また、 Tree でも interface を記述した。
+
+\lstinputlisting[label=src:agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda.replaced}
+
+interface を記述することによって、データを push する際に予め決まっている引数を省
+略することができた。
 また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確
 化された。
+
 % 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
 % する可能性があったが、 pushStack では紐付けた Stack に push することになり
 
-
 \section{継続を使った Agda における Test , Debug}
 
 Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
-しも期待した動作をするとは限らない。そのため、本研究中書いたプログラムが正しい動
+しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
 作をしているかを確認するために行なった手法を幾つか示す。
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -91,25 +126,35 @@
 かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
 いるかを確認している。
 
-このチェックでエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
-と、 push した値が Stack 上から消えることなく push した順番に取り出せるているこ
-とが分かる。
+この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
+と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
+かる。
+
+
+また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
+とができた。
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
+ができる。
+% \ref{sintax}のようなコードを
+% \begin{lstlisting}[frame=lrbt,label=sintax,caption={\footnotesize 通常の継続の
+%     コード}]
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-また今回、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
-とができた。
+% \end{lstlisting}
+
+% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={\footnotesize 糖衣構文
+%     を用いた継続のコード}]
+
+% \end{lstlisting}
 
 ソースコード~\ref{src:agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
 (Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
 また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
-とで、計算途中のデータの中身を確認することができた。
+とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。
 
-% \lstinputlisting[label=agda-tree-test, caption=Agdaにおけるテスト]{src/redBlackTreeTest.agda.replaced}
+ \lstinputlisting[label=src:agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda.replaced}
 
-評価結果はソースコード内にコメントで記述した。
-今回、この手法を用いることで複数関数を組み合わせた findNode 関数内に異常があるこ
+今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
 とが分かった。
 
 
@@ -117,5 +162,3 @@
 
 % \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda.replaced}
 % Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

--- a/final_main/chapter5.tex	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/chapter5.tex	Sun Feb 18 21:43:41 2018 +0900
@@ -2,7 +2,7 @@
 
 前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード
 を Agda にマッピングし等価なコードを生成できることを示した。
-本章では前章で作成した Interface の Stack や Tree のコードを使い Agda で
+本章では前章で生成した Interface の Stack や Tree のコードを使い Agda で
 Interface を経由したコードでの証明が可能であることを示す。
 
 % Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。
@@ -10,28 +10,46 @@
 % んな感じにするとできるのでは？っていう感じにしよ
 
 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
+\label{agda-interface-stack}
 
 % Stack の仕様記述
+ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
 
-Stack 
+Stack の処理として様々な性質が存在する。例えば、
 
-この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じものが受け取れる
-ことを証明している。
+\begin{itemize}
+ \item Stack に push した値は存在する
+ \item Stack に push した値は取り出すことができる
+ \item Stack に push した値を pop した時、その値は Stack から消える
+ \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない
+ \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する
+\end{itemize}
+
+などの性質がある。
 
-stackInSomeState 型は中身の分からない抽象的な Stack を作成している。リスト
-\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を2回
-行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
-る。
+本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前
+に入れた値と一致する」という性質を証明する。
+
+% この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ
+% ものが受け取れることを 証明している。
+
+まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state}
+の line1~2 で定義している stackInSomeState が不定状態の Stack である。
+ stackInSomeState 型は中身の分からない抽象的な Stack を作成している。ソースコー
+ ド~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
+ 2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
+ る。
+
+ \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush->push->pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
+ 
 % Agda でも継続を使った書き方で Interface 部分の実装を示した。
 
-\lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義と
-push->push->pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
-
 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
 型に書かれている。
 
+% この辺ちょっと怪しい感じ
 この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと
 めて refl で推論が通る。
 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
@@ -40,24 +58,63 @@
 
 % \lstinputlisting[label=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced}
 
-\section{Agda による Interface 部分を含めた Tree の部分的な証明}
+\section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題}
+ここでは Binary Tree の性質の一部に対して証明を行う。
+Binary Tree の性質として挙げられるのは次のようなものである
+% 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる
+
+\begin{itemize}
+ \item Tree に対して Node を Put することができる。
+ \item Tree に Put された Node は Delete されるまでなくならない。
+ \item Tree に 存在する Node とその子の関係は必ず「右の子 > Node」かつ「Node > 左の子」の関係になっている。
+ \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
+ \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
+\end{itemize}
+
+ここで証明する性質は
+
+${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
 
 
+\lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証
+明]{src/AgdaTreeProof.agda.replaced}
+
+この Tree の証明では、不定状態の redBlackInSomeState 型を作成し、その状態の Tree
+に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
+である。
+しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
+Node が存在するのか、 Get した Node と Put した Node が合同なのか等の様々な補
+題を証明し、全てが成り立つ必要がある。今回この証明では Put した Node と Get した
+Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
+同であることを示すことが困難であった。
+
+そのため、今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
+行おうと考えている。
 
 \section{Hoare Logic}
+\label{hoare-logic}
 
 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
-しさを推論する手法である。P を前状態(Precondition) 、C を処理(Command) 、 Q を
-後状態(Postcondition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
-プログラムは前状態を満たした後、処理を行い状態が後状態に変化する、といった形になる。
+しさを推論する手法である。P を前状態(PreCondition) 、C を処理(Command) 、 Q を
+後状態(PostCondition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
+プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といっ
+た形で考える事ができる。
 
-このとき、後状態から前状態を推論することが〜...
+このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
+動きをすることを証明することができる。
+この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
+PreCondition が CodeGear に入力として与えられる Input DataGear、Command が
+CodeGear、 PostCondition を Output DataGear として当てはめることができると考えて
+いる。
 
-Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
-最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
+
+今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ、
+幾つかの実装を証明していく。
+
+% Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
+% 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
 
 %%
 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
 % 入した。
-%%
-
+%%
\ No newline at end of file

--- a/final_main/chapter6.tex	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/chapter6.tex	Sun Feb 18 21:43:41 2018 +0900
@@ -1,2 +1,10 @@
-\chapter{まとめ}
+\chapter{今後の課題}
 
+本研究では CodeGear、 DataGear を用いたプログラミング手法を使い、Agda で
+Interface を用いたプログラムを実装し、検証した。これにより、 CbC で記述した時に
+は細かく分かっていなかった Interface の型が明確になった。
+また、研究の中にに継続を利用することで得られた知見は、今後の研究で大いに役立つと
+考えている。。
+
+今後の課題は、CodeGear、DataGear をベースにした Hoare Logic を Agda で実装する。
+また、その Hoare Logic を使い、いくつかの証明を実際に記述する。
\ No newline at end of file

Binary file final_main/main.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaSingleLinkedStack.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
@@ -0,0 +1,63 @@
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+push = pushSingleLinkedStack
+; pop  = popSingleLinkedStack
+; pop2 = pop2SingleLinkedStack
+; get  = getSingleLinkedStack
+; get2 = get2SingleLinkedStack
+; clear = clearSingleLinkedStack
+}
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+stack = emptySingleLinkedStack ;
+stackMethods = singleLinkedStackSpec
+}
+
+-- Implementation
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
+clearSingleLinkedStack stack next = next (record {top = Nothing})

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTree.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
@@ -0,0 +1,70 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
+data Color {n : Level } : Set n where
+  Red   : Color
+  Black : Color
+
+data CompareResult {n : Level } : Set n where
+  LT : CompareResult
+  GT : CompareResult
+  EQ : CompareResult
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+    field
+      key   : k
+      value : a
+      right : Maybe (Node a k)
+      left  : Maybe (Node a k)
+      color : Color {n}
+open Node
+
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
+
+open RedBlackTree
+
+
+leafNode : {n : Level } {a k : Set n}  @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
+leafNode k1 value = record {
+    key   = k1 ;
+    value = value ;
+    right = Nothing ;
+    left  = Nothing ;
+    color = Red
+  }
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
+
+getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ t) @$\rightarrow$@ t
+getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
+  module GetRedBlackTree where 
+    search : Node a k @$\rightarrow$@ t
+    checkNode : Maybe (Node a k) @$\rightarrow$@ t
+    checkNode Nothing = cs tree Nothing
+    checkNode (Just n) = search n
+    search n with compare tree k1 (key n) 
+    search n | LT = checkNode (left n)
+    search n | GT = checkNode (right n)
+    search n | EQ = cs tree (Just n)

--- a/final_main/src/AgdaTreeDebug.agda	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/src/AgdaTreeDebug.agda	Sun Feb 18 21:43:41 2018 +0900
@@ -1,6 +1,15 @@
 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
-$ \t -> putTree1 t 2 2
-$ \t -> putTree1 t 3 3
-$ \t -> putTree1 t 4 4
-$ \t -> getRedBlackTree t 4
-$ \t x -> x
+  $ \t -> putTree1 t 2 2
+  $ \t -> putTree1 t 3 3
+  $ \t -> putTree1 t 4 4
+  $ \t -> getRedBlackTree t 4
+  $ \t x -> x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTreeDebug.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
+  $ \t @$\rightarrow$@ putTree1 t 2 2
+  $ \t @$\rightarrow$@ putTree1 t 3 3
+  $ \t @$\rightarrow$@ putTree1 t 4 4
+  $ \t @$\rightarrow$@ getRedBlackTree t 4
+  $ \t x @$\rightarrow$@ x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })

--- a/final_main/src/AgdaTreeProof.agda	Fri Feb 16 16:58:40 2018 +0900
+++ b/final_main/src/AgdaTreeProof.agda	Sun Feb 18 21:43:41 2018 +0900
@@ -1,4 +1,4 @@
-module AgdaTreeTest where
+module AgdaTreeProof where
 
 open import RedBlackTree
 open import stack

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTreeProof.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
@@ -0,0 +1,107 @@
+module AgdaTreeTest where
+
+open import RedBlackTree
+open import stack
+open import Level hiding (zero)
+
+open import Data.Nat
+
+open Tree
+open Node
+open RedBlackTree.RedBlackTree
+open Stack
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Function
+
+check1 : {m : Level } (n : Maybe (Node  @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m}
+check1 Nothing _ = False
+check1 (Just n)  x with Data.Nat.compare (value n)  x
+...  | equal _ = True
+...  | _ = False
+
+check2 : {m : Level } (n : Maybe (Node  @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m}
+check2 Nothing _ = False
+check2 (Just n)  x with compare2 (value n)  x
+...  | EQ = True
+...  | _ = False
+
+putTree1 : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
+putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ replaceNode tree1 s n1 next))
+
+open @$\equiv$@-Reasoning
+
+redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+
+putTest1Lemma2 : (k : @$\mathbb{N}$@)  @$\rightarrow$@ compare2 k k @$\equiv$@ EQ
+putTest1Lemma2 zero = refl
+putTest1Lemma2 (suc k) = putTest1Lemma2 k
+
+putTest1Lemma1 : (x y : @$\mathbb{N}$@)  @$\rightarrow$@ compare@$\mathbb{N}$@ x y @$\equiv$@ compare2 x y
+putTest1Lemma1 zero    zero    = refl
+putTest1Lemma1 (suc m) zero    = refl
+putTest1Lemma1 zero    (suc n) = refl
+putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
+putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
+ where
+    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ LT  @$\equiv$@ compare2 m (@$\mathbb{N}$@.suc (m + k))
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
+ where
+    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ EQ  @$\equiv$@ compare2 m m
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
+ where
+    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ GT  @$\equiv$@ compare2  (@$\mathbb{N}$@.suc (m + k))  m
+    lemma1  zero = refl
+    lemma1  (suc y) = lemma1 y
+
+putTest1Lemma3 : (k : @$\mathbb{N}$@)  @$\rightarrow$@ compare@$\mathbb{N}$@ k k @$\equiv$@ EQ
+putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )
+
+compareLemma1 : {x  y : @$\mathbb{N}$@}  @$\rightarrow$@ compare2 x y @$\equiv$@ EQ @$\rightarrow$@ x  @$\equiv$@ y
+compareLemma1 {zero} {zero} refl = refl
+compareLemma1 {zero} {suc _} ()
+compareLemma1 {suc _} {zero} ()
+compareLemma1 {suc x} {suc y} eq = cong ( \z @$\rightarrow$@ @$\mathbb{N}$@.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
+   where
+      lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y
+      lemma2 = refl
+
+putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
+         @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
+         @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
+         (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True))
+putTest1 n k x with n
+...  | Just n1 = lemma2 ( record { top = Nothing } )
+   where
+     lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t))
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 {!!}
+        where
+           lemma3 : compare2 k (key n1) @$\equiv$@  EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
+               } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+           lemma3 eq with compare2 x x | putTest1Lemma2 x
+           ... | EQ | refl with compare2 k (key n1)  | eq
+           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
+           ...                    | EQ | refl = refl
+     ... |  GT = {!!}
+     ... |  LT = {!!}
+
+...  | Nothing =  lemma1
+   where
+     lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k
+        ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
+     lemma1 with compare2 k k | putTest1Lemma2 k
+     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
+     ...              | EQ | refl = refl

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/Goto.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
@@ -0,0 +1,4 @@
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+   @$\rightarrow$@ CodeSegment I O @$\rightarrow$@ I @$\rightarrow$@ O
+goto (cs b) i = b i
+