\section{今後の課題}
今後の課題として、以下が挙げられる。
RedBlackTree の基本操作として insert や delete が挙げられる。
通常は、再代入などを用いて実装を行うと思われるが、Agda が変数への代入を許していないため、
操作後の RedBlackTree を再構成するように実装を行う必要がある。
その際にどこの状態の検証を行うかが課題になっている。

先行研究にて、
個々の Code Gear の条件を書いてそれを接続することは Agda で実装されている。
しかし、接続された条件が健全であるか証明されていない。

証明されていない部分というのは、プログラム全体はいくつかの Code Gear の集まりだが、
Code Gear 実行後の事後条件が正しく次に実行される Code Gear の事前条件として成り立っているか、
それが最初からプログラムの停止まで正しく行われているかという部分である。

今後はこの接続された条件の健全性の証明から行っていく。