--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/future.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -0,0 +1,12 @@
+\section{今後の課題}
+今後の課題として、以下が挙げられる。
+赤黒木の基本操作として insert や delete が挙げられる。
+通常は、再代入などを用いて実装を行うと思われるが、agda が変数への代入を許していないため、
+操作後の赤黒木を再構成するように実装を行う必要がある。
+その際にどこの状態の検証を行うかが課題になっている。
+
+先行研究にて、
+個々の Code Gear の条件を書いてそれを接続することは agda で実装されている。
+しかし、接続された条件が健全であるか証明されていない。
+
+今後はこの接続された条件の健全性の証明からしていく。