Binary file Report/final/.DS_Store has changed

--- a/Report/final/text/chapter2.tex	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/text/chapter2.tex	Mon Jan 29 19:48:21 2024 +0900
@@ -27,7 +27,7 @@
    \label{BinarySearchTree.png}
    \end{center}
 \end{figure}
-図\ref{BinarySearchTree.png}を見ると前述した制約が満たされていることがわかる．また，赤いノードから見た青のノードは親子関係であり，赤ノードから見た緑ノードは叔父に当たることがわかる．
+図\ref{BinarySearchTree.png}を見ると前述した制約が満たされていることがわかる．また，赤いノードから見た青のノードは親子関係であり，赤ノードから見た緑ノードはおじに当たることがわかる．
 本研究の対象であるRedBlackTreeの元となる木構造となっている．
 \section{RedBlackTree}
 RedBlackTree とは，GearsOS に採用される予定のあるバランスした二分探索木の一種である．
@@ -48,7 +48,7 @@
    \end{center}
 \end{figure}
 
-特に４つ目の制約により，RedBlackTreeがある程度の平衡性を持っていることが確認できる．挿入・削除・検索といった操作は最悪のケースでは木の高さに比例した計算時間をようするが，RedBlackTreeは黒の深さで木の高さが平衡しているため，最悪のケースにおける計算量が，データの挿入・削除・検索のいずれにおいても，データ構造のうちで最善のものの一つであるという利点がある．また，木の深さがバランスしていない場合は，親と叔父の色\input{../../Report}
+特に４つ目の制約により，RedBlackTreeがある程度の平衡性を持っていることが確認できる．挿入・削除・検索といった操作は最悪のケースでは木の高さに比例した計算時間をようするが，RedBlackTreeは黒の深さで木の高さが平衡しているため，最悪のケースにおける計算量が，データの挿入・削除・検索のいずれにおいても，データ構造のうちで最善のものの一つであるという利点がある．また，木の深さがバランスしていない場合は，親とおじの色\input{../../Report}
 を見て木を回転させるという操作が必要になる．
 
 \section{Agda}

--- a/Report/final/text/chapter5.tex	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/text/chapter5.tex	Mon Jan 29 19:48:21 2024 +0900
@@ -96,7 +96,7 @@
 		testRBTree0	& 図\ref{RedBlackTree.png}で示したRedBlackTreeをGearsAgda上で表した関数．\\
 		testRBI0	& testRBTree0のRBtreeInvariantを意味する．\\
 		\hline
-		result		& record型である，C言語でいう構造体である．findの結果を格納するために使用する．\\
+		result		& record型と呼ばれるもの．C言語でいう構造体である．\\
 		\hline
 	\end{tabular}
 \end{table}

--- a/Report/final/text/chapter6.aux	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/text/chapter6.aux	Mon Jan 29 19:48:21 2024 +0900
@@ -1,11 +1,20 @@
 \relax 
+<<<<<<< HEAD
+\@writefile{toc}{\contentsline {chapter}{\numberline {第6章}RedBlackTreeにおけるInsert操作}{26}{}\protected@file@percent }
+=======
 \@writefile{toc}{\contentsline {chapter}{\numberline {第6章}まとめと今後の展望}{26}\protected@file@percent }
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4
 \@writefile{lof}{\addvspace {10\jsc@mpt }}
 \@writefile{lot}{\addvspace {10\jsc@mpt }}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Insertのアルゴリズム}{26}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Insertの場合分け}{26}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Insertの場合分け}}{27}{}\protected@file@percent }
+\newlabel{InsertCase.png}{{6.1}{27}{}{}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}GearsAgdaによるInsertの実装}{29}{}\protected@file@percent }
 \@setckpt{./text/chapter6}{
-\setcounter{page}{27}
+\setcounter{page}{30}
 \setcounter{equation}{0}
-\setcounter{enumi}{2}
+\setcounter{enumi}{3}
 \setcounter{enumii}{0}
 \setcounter{enumiii}{0}
 \setcounter{enumiv}{0}
@@ -13,12 +22,12 @@
 \setcounter{mpfootnote}{0}
 \setcounter{part}{0}
 \setcounter{chapter}{6}
-\setcounter{section}{0}
+\setcounter{section}{3}
 \setcounter{subsection}{0}
 \setcounter{subsubsection}{0}
 \setcounter{paragraph}{0}
 \setcounter{subparagraph}{0}
-\setcounter{figure}{0}
+\setcounter{figure}{1}
 \setcounter{table}{0}
 \setcounter{parentequation}{0}
 \setcounter{lstnumber}{20}

--- a/Report/final/text/chapter6.tex	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/text/chapter6.tex	Mon Jan 29 19:48:21 2024 +0900
@@ -1,7 +1,66 @@
-\chapter{まとめと今後の展望}
+\chapter{RedBlackTreeにおけるInsert操作}
+本章では、RedBlackTreeのInsert操作について解説していく。なお、現段階では証明付き実装には至っていない。したがって、RedBlackTreeのInsertにおける大まかなアルゴリズムや実装方法について解説していく。
+
+\section{Insertのアルゴリズム}
+Insertとは、新しいノードを木に追加する操作である。RedBlackTreeでは、Insertされるノードは赤として扱い、黒の深さがバランスしているという特徴を持つことから、Insertによって黒の深さが崩れてしまう場合、それを補うように木を回転させる必要がある。したがって、RedBlackTreeのInsertには以下の手順が必要になる。
+
+\begin{enumerate}
+\item Insertするノードのkeyを見て、Insertする位置を特定する。
+\item Insertする位置からみて、親、祖父母、おじのノードの色を特定する。
+\item 各ノードの色パターンに応じた、木の回転や色の置き換えなどの操作を行う。
+\end{enumerate}
 
-本論文では，GearsAgdaを用いたプログラムを数学的に証明する方法とRedBlackTreeの正当性をInvariantを用いて証明する実装について述べた．GearsAgdaを用いて再帰処理を使用しない記述を実装することで，GearsOSに使用されているCbC言語に直接対応するような証明を書くことが可能になった．また，Invariantを定義し，それらを保有しながら処理を行うことにより，数学的な証明を用いてRedBlackTreeの信頼性を向上させることができた．このInvariantからは，さまざまな要素を導出できることから，今後の研究において応用的な処理を記述する際にも役立つと考える．
+上記に示した通り、Insertする位置と各ノードの色によって場合分けし操作を変える必要がある。
+
+\section{Insertの場合分け}
+Insertの場合分けの数は６パターンあると考えられており、以下に表としてそれをまとめる。
+\clearpage
+\begin{figure}[htbp]
+  \begin{center}
+   \includegraphics[width=100mm]{./figs/InsertCase.png}
+   \caption[Insertの場合分け]{Insertの場合分け}
+   \label{InsertCase.png}
+   \end{center}
+\end{figure}
 
-今後の課題として，Insert，deleteのなどの操作を実装することが挙げられる．現段階で証明されている操作はfindしかなく，これでは実用的なRedBlackTreeとは言えない．Insertの実装は大きな枠組みは既に完成しており，証明部分を記述していく段階である．しかし，Insertなどの木構造を変化させる操作では，木がバランスする動作を記述する必要があり，子供から見た祖父や叔父の色を見ながら場合わけをする必要がある．これにより，場合わけの数が多く実装が難しくなっているのが現状である．Insertを実装することができれば，似たようなアルゴリズムでdeleteを実装できるため，まずはInsertを簡単に記述する方法を探しつつ，着実に実装を進めていく必要がある．
+図\ref{InsertCase.png}の各列の意味を箇条書きで説明する。
+\begin{itemize}
+\item 前の状態 : 木に操作を施す前の各ノードの状態を表す。P、G、Uはそれぞれ親、祖父母、おじの意味を持つ。x列は子の向きの変化を表し、o（外側）はPとNがともに左またはともに右の子であることを意味し、i（内側）はPからNへの方向がGからPへの方向と違うことを意味する。
+\item ケース : 適応する操作の種類を示している。詳細については後述する。
+\item 回転 : バランスする際に木を回転する必要があるかを示している。
+\item 割り当て : 次の操作に遷移する際に、注目するノードＮが変化することを表している。
+\item 後の状態 : ケースによってノードに変更があった場合、各ノードの後の状態を示している。?は後の状態が１つに定まらないことを意味している。
+\item 次 : 木がバランスしてない場合に行う次の操作を示している。「-」となっている場合、木のバランスが完了したことを意味する。
+\end{itemize}
+
+以上に記した通り、RedBlackTreeのInsert操作は６パターンの操作が考えられる。また、ケースI2では後の状態が定まっていない。これは、注目するノードNが祖父母にまで上ることで祖父母から見たパターンマッチを再度行う必要があるからである。このように、RedBlackTreeのInsertでは、注目するノードＮが場合によって変化することで、操作が複雑になってしまうことが考えられる。
+次に、これらのInsertCaseごとの動作を説明していく。
+
+InsertCase1では、親ノードが黒、祖父母ノードがNULL、おじノードがNULLの場合を考える。この場合では、親以外のノードが存在しないため、親ノードの色に応じて操作を考える。ここで、親ノードは黒、Insertされるノードは赤であるため、親ノードの子としてそのままInsertして問題がない。したがって、InsertCase1ではそのまま親ノードの子としてInsertを実行することができる。
+\\
+
+InsertCase2では、親ノードが赤、祖父母ノードが黒、おじノードが赤の場合を考える。この場合では、親ノードの下にそのままInsertすると赤が連続してしまう。したがって、親とおじの色を両方黒に変更し、祖父母の色を赤にすることでバランスする。このとき、祖父母の親ノードが赤色の場合に赤が連続してしまう可能性があるため、注目するノードNを祖父母ノードに変更し、１つ上の黒のノードまで戻る必要がある。戻った際の木の状態が未定のため、後の状態と次の遷移先は再度場合分けをする必要がある。
+\\
 
-今後の展望として，GearsAgdaのコードをCbCのコードに変換することが挙げられる．GearsAgdaはCbCに直接対応した記述方法であるため，理論上コンパイルすることが可能である．CbC言語はC言語とアセンブラの中間に位置しており，コーディングが困難であることから，GearsAgdaを用いてコーディングできることが望ましい．これが可能になることで，CbCでの記述がGearsAgdaベースで行えるようになり，信頼性のさらなる向上につながると考える．
\ No newline at end of file
+InsertCase3では、注目するノードNしか存在していないため、そのまま挿入することができる。
+\\
+
+InsertCase4では、親ノードが赤、祖父母ノードがNULL、おじノードがNULLの場合を考える。この場合では、親以外のノードが存在しないため、親ノードの色に応じて操作を考える。ここで、親ノードは赤、Insertされるノードは赤であるため、親ノードの子としてそのままInsertしてしまうと赤が連続してしまい、制約に反する。したがって、InsertCase4では親ノードの色を黒に変更し、子ノードとしてInsertすることができる。
+\\
+
+InsertCase5では、親ノードが赤、祖父母ノードが黒、おじノードが黒の場合を考える。この場合では、親ノードの下にそのままInsertすると赤が連続してしまう。したがって、バランスするために木を回転させる必要があるが、xの値がiであり、木が内側に曲がっているため、木の回転がうまくいかない。このとき、一度親と子の間で回転を行い、xの値をoに変更する操作が必要になる。この操作を終えた後の状態はInsertCase6と一致するため、InsertCase5はInsertCase6に遷移することが確認できる。まとめると、InsertCase5はInsertCase6に遷移するための下準備を行っていると言える。
+\\
+
+InsertCase6では、親ノードが赤、祖父母ノードが黒、おじノードが黒の場合を考える。この場合では、親ノードの下にそのままInsertすると赤が連続してしまう。そのため、祖父母ノードと親ノードの間で木の回転を行い、親ノードを黒に、祖父母ノードを赤に変更することで木をバランスさせる。
+\\
+
+以上の６パターンの操作を組み合わせることでRedBlackTreeのバランスを保つことができる。特に注目するべき点はInsertCase2であり、この場合は次の遷移先が未定であるため、どこに遷移するかを明らかにする処理が必要になると考えられる。
+
+\section{GearsAgdaによるInsertの実装}
+ここでは、GearsAgdaでのInsert操作を実装に関して述べていく。現状として、Insert操作の証明付き実装には至っていない。実装を困難にしている理由として以下のことが考えられる。
+\begin{itemize}
+\item 場合分けの数が多い
+\item 様々なInvariantを用いるため、証明の数が多い
+\item GearsAgdaでの実装によるコーディングの煩雑化
+\end{itemize}
+まず、場合分けの数が多いことが挙げられる。これは、InsertCase事態の数も多いが、1つのCaseを記述するためにKeyの大小を比較など様々な場合分けが必要になり、その都度違う処理を記述する必要があることが実装を困難にしている。また、Invariantを用いての証明になるため、Invariantごとにも場合分けも行う必要がある。これを解決するためには、すべての場合とその条件を見つめなおし整理することや、場合分けが被らないよう気を付けながらコーディングする必要がある。次に、様々なInvariantを用いるため、証明の数が多いことが挙げられる。これは、Invariantを示す際の引数に対してそれぞれの証明を入れる必要があるが、その数が多く一つ一つが複雑であるため、コーディングを困難にしている。また、Invariant事態の内容が間違っている可能性もある。Invariantは表示的意味論であるため証明の本質は変わらないが、入力として受ける内容などが間違っていた場合、コードの修正は自明ではない。これを解決するためには、Invariantの内容や性質を深く理解し、そこから導出される事柄について理解し、証明を簡易化していくことが必要である。最後に、GearsAgdaでの実装によるコーディングの煩雑化が挙げられる。GearsAgdaはCbC言語の特徴を受け継いでいることから様々な制限が設けられており、コーディングを難しくしている。また、一般的なプログラミング言語のような可読性が無いことも要因として考えられる。これを解決するためには、GearsAgdaの軽量継続の理解をより深め、全体的な構造を理解することなどが考えられる。
\ No newline at end of file

--- a/Report/final/text/reference.aux	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/text/reference.aux	Mon Jan 29 19:48:21 2024 +0900
@@ -4,18 +4,22 @@
 \bibcite{agdawiki}{3}
 \bibcite{agdadocument}{4}
 \bibcite{ueti}{5}
+<<<<<<< HEAD
+\@writefile{toc}{\contentsline {chapter}{参考文献}{32}{}\protected@file@percent }
+=======
 \@writefile{toc}{\contentsline {chapter}{参考文献}{28}\protected@file@percent }
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4
 \@setckpt{./text/reference}{
-\setcounter{page}{29}
+\setcounter{page}{33}
 \setcounter{equation}{0}
-\setcounter{enumi}{2}
+\setcounter{enumi}{3}
 \setcounter{enumii}{0}
 \setcounter{enumiii}{0}
 \setcounter{enumiv}{5}
 \setcounter{footnote}{0}
 \setcounter{mpfootnote}{0}
 \setcounter{part}{0}
-\setcounter{chapter}{6}
+\setcounter{chapter}{7}
 \setcounter{section}{0}
 \setcounter{subsection}{0}
 \setcounter{subsubsection}{0}

--- a/Report/final/thesis.aux	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.aux	Mon Jan 29 19:48:21 2024 +0900
@@ -5,4 +5,9 @@
 \@input{./text/chapter4.aux}
 \@input{./text/chapter5.aux}
 \@input{./text/chapter6.aux}
+\@input{./text/chapter7.aux}
 \@input{./text/reference.aux}
+<<<<<<< HEAD
+\gdef \@abspage@last{40}
+=======
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4

--- a/Report/final/thesis.lof	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.lof	Mon Jan 29 19:48:21 2024 +0900
@@ -6,3 +6,5 @@
 \addvspace {10\jsc@mpt }
 \addvspace {10\jsc@mpt }
 \addvspace {10\jsc@mpt }
+\contentsline {figure}{\numberline {6.1}{\ignorespaces Insertの場合分け}}{27}{}%
+\addvspace {10\jsc@mpt }

--- a/Report/final/thesis.log	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.log	Mon Jan 29 19:48:21 2024 +0900
@@ -1,4 +1,8 @@
+<<<<<<< HEAD
+This is e-upTeX, Version 3.141592653-p4.1.0-u1.29-230214-2.6 (utf8.sjis) (TeX Live 2023) (preloaded format=platex 2023.7.24)  23 JAN 2024 00:36
+=======
 This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.4.14)  22 JAN 2024 10:17
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -519,7 +523,7 @@
 
 (./thesis.aux (./text/introduction.aux) (./text/chapter2.aux)
 (./text/chapter3.aux) (./text/chapter4.aux) (./text/chapter5.aux)
-(./text/chapter6.aux) (./text/reference.aux))
+(./text/chapter6.aux) (./text/chapter7.aux) (./text/reference.aux))
 \openout1 = `thesis.aux'.
 
 LaTeX Font Info:    Checking defaults for OML/txmi/m/it on input line 72.
@@ -836,6 +840,9 @@
 
 [19
 
+<<<<<<< HEAD
+] [20] [21] [22
+=======
 ] [20]
 Overfull \hbox (87.32846pt too wide) in paragraph at lines 89--102
  [][][][] 
@@ -847,6 +854,7 @@
  (/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/ts1txtt.fd
 File: ts1txtt.fd 2000/12/15 v3.1
 ) [22
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4
 
 ]
 [23] [24]) [25]
@@ -854,11 +862,36 @@
 
  (./text/chapter6.tex
 第6章
-) [26
+[26
 
 
 
+<<<<<<< HEAD
+
+]
+File: ./figs/InsertCase.png Graphic file (type bmp)
+<./figs/InsertCase.png>
+LaTeX Font Info:    Trying to load font information for TS1+txr on input line 2
+8.
+ (c:/texlive/2023/texmf-dist/tex/latex/txfonts/ts1txr.fd
+File: ts1txr.fd 2000/12/15 v3.1
+) [27
+
+] [28])
+[29]
+\openout2 = `./text/chapter7.aux'.
+
+ (./text/chapter7.tex
+第7章
+) [30
+
+
+
+
+] [31
+=======
 ] [27
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4
 
 
 ]
@@ -870,11 +903,30 @@
 u-rial repos-i-tory, http://www. cr.ie.u-
  []
 
-) [28
+) [32
 
 
 ] (./thesis.aux (./text/introduction.aux) (./text/chapter2.aux)
 (./text/chapter3.aux) (./text/chapter4.aux) (./text/chapter5.aux)
+<<<<<<< HEAD
+(./text/chapter6.aux) (./text/chapter7.aux) (./text/reference.aux))
+ ***********
+pLaTeX2e <2023-02-14>+1, based on
+LaTeX2e <2023-06-01> patch level 1
+L3 programming layer <2023-06-30>
+ ***********
+ ) 
+Here is how much of TeX's memory you used:
+ 7854 strings out of 475891
+ 110451 string characters out of 5782800
+ 2143074 words of memory out of 5000000
+ 28936 multiletter control sequences out of 15000+600000
+ 589551 words of font info for 144 fonts, out of 8000000 for 9000
+ 934 hyphenation exceptions out of 8191
+ 72i,12n,79p,1381b,1886s stack positions out of 10000i,1000n,20000p,200000b,200000s
+
+Output written on thesis.dvi (40 pages, 137456 bytes).
+=======
 (./text/chapter6.aux) (./text/reference.aux))
 
 LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
@@ -890,3 +942,4 @@
  36i,12n,45p,675b,1839s stack positions out of 5000i,500n,10000p,200000b,80000s
 
 Output written on thesis.dvi (36 pages, 121092 bytes).
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4

--- a/Report/final/thesis.lot	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.lot	Mon Jan 29 19:48:21 2024 +0900
@@ -6,3 +6,4 @@
 \contentsline {table}{\numberline {5.1}{\ignorespaces findRBTに使用される関数}}{19}% 
 \contentsline {table}{\numberline {5.2}{\ignorespaces findTestに使用される関数}}{21}% 
 \addvspace {10\jsc@mpt }
+\addvspace {10\jsc@mpt }

Binary file Report/final/thesis.pdf has changed

Binary file Report/final/thesis.synctex.gz has changed

--- a/Report/final/thesis.tex	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.tex	Mon Jan 29 19:48:21 2024 +0900
@@ -101,6 +101,8 @@
 \include{./text/chapter5}
 
 \include{./text/chapter6}
+
+\include{./text/chapter7}
 \chapter*{謝辞}
 本研究の遂行，本論文の作成にあたり，御多忙にも関わらず終始懇切丁寧なる御指導と御教授を賜わりました，河野真治准教授に心より感謝致します．そして，共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します．最後に，有意義な時間を共に過ごした知能情報コースの学友，並びに物心両面で支えてくれた家族に深く感謝致します．
 \begin{flushright}

--- a/Report/final/thesis.toc	Mon Jan 22 10:27:20 2024 +0900
+++ b/Report/final/thesis.toc	Mon Jan 29 19:48:21 2024 +0900
@@ -1,3 +1,37 @@
+<<<<<<< HEAD
+\contentsline {chapter}{\numberline {第1章}プログラムの信頼性}{1}{}%
+\contentsline {section}{\numberline {1.1}背景と目的}{1}{}%
+\contentsline {section}{\numberline {1.2}論文の構成}{2}{}%
+\contentsline {chapter}{\numberline {第2章}基礎概念}{3}{}%
+\contentsline {section}{\numberline {2.1}CbC}{3}{}%
+\contentsline {section}{\numberline {2.2}GearsOS}{3}{}%
+\contentsline {section}{\numberline {2.3}BinarySearchTree}{4}{}%
+\contentsline {section}{\numberline {2.4}RedBlackTree}{4}{}%
+\contentsline {section}{\numberline {2.5}Agda}{5}{}%
+\contentsline {subsection}{\numberline {2.5.1}Data型の実装}{6}{}%
+\contentsline {subsection}{\numberline {2.5.2}関数の実装}{6}{}%
+\contentsline {subsection}{\numberline {2.5.3}場合分けの書き方}{7}{}%
+\contentsline {section}{\numberline {2.6}GearsAgda}{8}{}%
+\contentsline {subsection}{\numberline {2.6.1}GearsAgdaの記述方法}{9}{}%
+\contentsline {chapter}{\numberline {第3章}提案手法}{11}{}%
+\contentsline {section}{\numberline {3.1}BinarySearchTreeを応用した，RedBlackTreeの実装}{11}{}%
+\contentsline {section}{\numberline {3.2}Invariantを見つける}{11}{}%
+\contentsline {chapter}{\numberline {第4章}RedBlackTreeとInvariantの実装}{12}{}%
+\contentsline {section}{\numberline {4.1}RedBlackTreeの基本的な実装}{12}{}%
+\contentsline {section}{\numberline {4.2}Invariantの実装}{14}{}%
+\contentsline {subsection}{\numberline {4.2.1}RBtreeInvariantの実装}{14}{}%
+\contentsline {subsection}{\numberline {4.2.2}stackInvariantの実装}{16}{}%
+\contentsline {chapter}{\numberline {第5章}findRBTの実行}{18}{}%
+\contentsline {section}{\numberline {5.1}findRBTの実装}{18}{}%
+\contentsline {section}{\numberline {5.2}findRBTの実行方法}{21}{}%
+\contentsline {section}{\numberline {5.3}実行結果}{23}{}%
+\contentsline {chapter}{\numberline {第6章}RedBlackTreeにおけるInsert操作}{26}{}%
+\contentsline {section}{\numberline {6.1}Insertのアルゴリズム}{26}{}%
+\contentsline {section}{\numberline {6.2}Insertの場合分け}{26}{}%
+\contentsline {section}{\numberline {6.3}GearsAgdaによるInsertの実装}{29}{}%
+\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{30}{}%
+\contentsline {chapter}{参考文献}{32}{}%
+=======
 \contentsline {chapter}{\numberline {第1章}プログラムの信頼性}{1}% 
 \contentsline {section}{\numberline {1.1}背景と目的}{1}% 
 \contentsline {section}{\numberline {1.2}論文の構成}{2}% 
@@ -26,3 +60,4 @@
 \contentsline {section}{\numberline {5.3}実行結果}{23}% 
 \contentsline {chapter}{\numberline {第6章}まとめと今後の展望}{26}% 
 \contentsline {chapter}{参考文献}{28}% 
+>>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4