--- a/paper/tex/rbt_verif.tex	Mon Feb 15 21:42:10 2021 +0900
+++ b/paper/tex/rbt_verif.tex	Mon Feb 15 23:36:39 2021 +0900
@@ -1,5 +1,6 @@
-\chapter{Red Black Tree の検証}
-実装が困難であったため、検証するまでには至らなかった。
+\chapter{Left Learning Red Black Tree の検証}
+本章では、Left Learning Red Black Tree の
+検証方法について述べる
 
 \section{Meta Data Gearの記述}
 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
@@ -46,13 +47,14 @@
 inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
 持った List となっている。
 
+これを Left Learning Red Black Tree の 仕様を満たすように、
+全てに対して行う。
+その後、条件が接続されているのかを検証したのち、健全性について示す事で
+Hoare Logic による検証ができる。
 
 
-以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。
 
 
-これを用いることで、各 node より上の node の大小関係を検証できると考えた。
-
 %\subsection{Black node の数え上げ}
 %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。