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

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

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