# HG changeset patch # User mori # Date 1707375002 -32400 # Node ID dd37dd73a8ea795a1a38fc6a02dc6a96f98d8d0a # Parent 70346fe80c78fdba70d5a8c34c518516df32f6ca fix diff -r 70346fe80c78 -r dd37dd73a8ea Report/.DS_Store Binary file Report/.DS_Store has changed diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/.DS_Store Binary file Report/final/.DS_Store has changed diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/refe/.DS_Store Binary file Report/final/refe/.DS_Store has changed diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter2.aux --- a/Report/final/text/chapter2.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第2章}基礎概念}{3}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@writefile{toc}{\contentsline {section}{\numberline {2.1}CbC}{3}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2.2}GearsOS}{3}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2.3}BinarySearchTree}{4}\protected@file@percent } -\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces BinarySearchTreeにおけるノード関係}}{4}\protected@file@percent } -\newlabel{BinarySearchTree.png}{{2.1}{4}} -\@writefile{toc}{\contentsline {section}{\numberline {2.4}RedBlackTree}{4}\protected@file@percent } -\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces RedBlackTreeにおけるノードの制約}}{5}\protected@file@percent } -\newlabel{RedBlackTree.png}{{2.2}{5}} -\@writefile{toc}{\contentsline {section}{\numberline {2.5}Agda}{5}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.5.1}Data型の実装}{6}\protected@file@percent } -\newlabel{Data.agda}{{2.1}{6}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}AgdaにおけるData型の実装}{6}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.5.2}関数の実装}{6}\protected@file@percent } -\newlabel{plus.agda}{{2.2}{6}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.2}Agdaにおける足し算の実装}{6}\protected@file@percent } -\newlabel{+.agda}{{2.3}{7}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.3}Agdにおける二項演算子の実装}{7}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.5.3}場合分けの書き方}{7}\protected@file@percent } -\newlabel{compare.agda}{{2.4}{7}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.4}Agdaにおける場合分けの書き方}{7}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2.6}GearsAgda}{8}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.6.1}GearsAgdaの記述方法}{9}\protected@file@percent } -\newlabel{gears.agda}{{2.5}{9}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.5}GearsAgdaにおける足し算の実装}{9}\protected@file@percent } -\@setckpt{./text/chapter2}{ -\setcounter{page}{11} -\setcounter{equation}{0} -\setcounter{enumi}{4} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{2} -\setcounter{section}{6} -\setcounter{subsection}{1} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{2} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{14} -\setcounter{lstlisting}{5} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter2.log --- a/Report/final/text/chapter2.log Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -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) 10 JAN 2024 00:28 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**chapter2.tex -(./chapter2.tex -pLaTeX2e <2023-02-14>+1, based on -LaTeX2e <2023-06-01> patch level 1 -L3 programming layer <2023-06-30> -! Undefined control sequence. -l.2 \chapter - {基礎概念} -? -! Emergency stop. -l.2 - -End of file on the terminal! - - -Here is how much of TeX's memory you used: - 17 strings out of 475891 - 333 string characters out of 5782800 - 1909074 words of memory out of 5000000 - 21367 multiletter control sequences out of 15000+600000 - 561940 words of font info for 53 fonts, out of 8000000 for 9000 - 929 hyphenation exceptions out of 8191 - 15i,0n,23p,47b,18s stack positions out of 10000i,1000n,20000p,200000b,200000s -No pages of output. diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter3.aux --- a/Report/final/text/chapter3.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}提案手法}{11}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@writefile{toc}{\contentsline {section}{\numberline {3.1}BinarySearchTreeを応用した，RedBlackTreeの実装}{11}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {3.2}Invariantを見つける}{11}\protected@file@percent } -\@setckpt{./text/chapter3}{ -\setcounter{page}{12} -\setcounter{equation}{0} -\setcounter{enumi}{2} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{3} -\setcounter{section}{2} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{14} -\setcounter{lstlisting}{0} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter3.log --- a/Report/final/text/chapter3.log Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -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) 11 JAN 2024 19:24 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**chapter3.tex -(./chapter3.tex -pLaTeX2e <2023-02-14>+1, based on -LaTeX2e <2023-06-01> patch level 1 -L3 programming layer <2023-06-30> -! Undefined control sequence. -l.1 \chapter - {提案手法} -? -! Emergency stop. -l.1 - -End of file on the terminal! - - -Here is how much of TeX's memory you used: - 17 strings out of 475891 - 333 string characters out of 5782800 - 1909074 words of memory out of 5000000 - 21367 multiletter control sequences out of 15000+600000 - 561940 words of font info for 53 fonts, out of 8000000 for 9000 - 929 hyphenation exceptions out of 8191 - 15i,0n,23p,65b,18s stack positions out of 10000i,1000n,20000p,200000b,200000s -No pages of output. diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter4.aux --- a/Report/final/text/chapter4.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}RedBlackTreeとInvariantの実装}{12}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@writefile{toc}{\contentsline {section}{\numberline {4.1}RedBlackTreeの基本的な実装}{12}\protected@file@percent } -\newlabel{bt.agda}{{4.1}{12}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.1}BinarySearchTreeの基本的な実装}{12}\protected@file@percent } -\newlabel{rbt.agda}{{4.2}{13}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.2}RedBlackTreeの基本的な実装}{13}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.2}Invariantの実装}{14}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.1}RBtreeInvariantの実装}{14}\protected@file@percent } -\newlabel{RBtreeInvariant.agda}{{4.3}{14}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.3}RBtreeInvariantの実装}{14}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {4.2.2}stackInvariantの実装}{16}\protected@file@percent } -\newlabel{stackInvariant.agda}{{4.4}{16}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.4}stackInvariantの実装}{16}\protected@file@percent } -\@setckpt{./text/chapter4}{ -\setcounter{page}{18} -\setcounter{equation}{0} -\setcounter{enumi}{2} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{4} -\setcounter{section}{2} -\setcounter{subsection}{2} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{11} -\setcounter{lstlisting}{4} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter4.log diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter5.aux --- a/Report/final/text/chapter5.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,41 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第5章}findRBTの実行}{18}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@writefile{toc}{\contentsline {section}{\numberline {5.1}findRBTの実装}{18}\protected@file@percent } -\@writefile{lot}{\contentsline {table}{\numberline {5.1}{\ignorespaces findRBTに使用される関数}}{19}\protected@file@percent } -\newlabel{findRBT}{{5.1}{19}} -\newlabel{findRBT.agda}{{5.1}{19}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}findRBTの実装}{19}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5.2}findRBTの実行方法}{21}\protected@file@percent } -\@writefile{lot}{\contentsline {table}{\numberline {5.2}{\ignorespaces findTestに使用される関数}}{21}\protected@file@percent } -\newlabel{findtest}{{5.2}{21}} -\newlabel{findTest.agda}{{5.2}{22}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.2}findTestの実装}{22}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5.3}実行結果}{23}\protected@file@percent } -\newlabel{result14}{{5.3}{23}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}Keyの値14のfindTest実行結果}{23}\protected@file@percent } -\newlabel{result1}{{5.4}{24}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}Keyの値1のfindTest実行結果}{24}\protected@file@percent } -\@setckpt{./text/chapter5}{ -\setcounter{page}{26} -\setcounter{equation}{0} -\setcounter{enumi}{2} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{5} -\setcounter{section}{3} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{2} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{20} -\setcounter{lstlisting}{4} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter6.aux --- a/Report/final/text/chapter6.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -\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}{30} -\setcounter{equation}{0} -\setcounter{enumi}{3} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{6} -\setcounter{section}{3} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{1} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{20} -\setcounter{lstlisting}{0} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/chapter7.aux --- a/Report/final/text/chapter7.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{30}{}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@setckpt{./text/chapter7}{ -\setcounter{page}{31} -\setcounter{equation}{0} -\setcounter{enumi}{3} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{7} -\setcounter{section}{0} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{20} -\setcounter{lstlisting}{0} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/introduction.aux --- a/Report/final/text/introduction.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第1章}プログラムの信頼性}{1}\protected@file@percent } -\@writefile{lof}{\addvspace {10\jsc@mpt }} -\@writefile{lot}{\addvspace {10\jsc@mpt }} -\@writefile{toc}{\contentsline {section}{\numberline {1.1}背景と目的}{1}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {1.2}論文の構成}{2}\protected@file@percent } -\@setckpt{./text/introduction}{ -\setcounter{page}{3} -\setcounter{equation}{0} -\setcounter{enumi}{0} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{0} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{1} -\setcounter{section}{2} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{1} -\setcounter{lstlisting}{0} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/text/reference.aux --- a/Report/final/text/reference.aux Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -\relax -\bibcite{HoareLogic}{1} -\bibcite{sotoma}{2} -\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}{33} -\setcounter{equation}{0} -\setcounter{enumi}{3} -\setcounter{enumii}{0} -\setcounter{enumiii}{0} -\setcounter{enumiv}{5} -\setcounter{footnote}{0} -\setcounter{mpfootnote}{0} -\setcounter{part}{0} -\setcounter{chapter}{7} -\setcounter{section}{0} -\setcounter{subsection}{0} -\setcounter{subsubsection}{0} -\setcounter{paragraph}{0} -\setcounter{subparagraph}{0} -\setcounter{figure}{0} -\setcounter{table}{0} -\setcounter{parentequation}{0} -\setcounter{lstnumber}{20} -\setcounter{lstlisting}{0} -} diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.lof --- a/Report/final/thesis.lof Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\contentsline {figure}{\numberline {2.1}{\ignorespaces BinarySearchTreeにおけるノード関係}}{4}% -\contentsline {figure}{\numberline {2.2}{\ignorespaces RedBlackTreeにおけるノードの制約}}{5}% -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\contentsline {figure}{\numberline {6.1}{\ignorespaces Insertの場合分け}}{27}{}% -\addvspace {10\jsc@mpt } diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.log --- a/Report/final/thesis.log Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,945 +0,0 @@ -<<<<<<< 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. - %&-line parsing enabled. -**thesis.tex -(./thesis.tex -pLaTeX2e <2019-04-06> (based on LaTeX2e <2018-12-01>) -(/usr/local/texlive/2019/texmf-dist/tex/platex/jsclasses/jsreport.cls -Document Class: jsreport 2019/04/06 jsclasses (okumura, texjporg) -\jsc@mpt=\dimen118 -\jsc@mmm=\dimen119 -\jsc@smallskipamount=\skip41 -LaTeX Info: Redefining \rmfamily on input line 467. -LaTeX Info: Redefining \sffamily on input line 470. -LaTeX Info: Redefining \ttfamily on input line 473. -LaTeX Info: Redefining \textmc on input line 477. -LaTeX Info: Redefining \textgt on input line 479. -\symmincho=\mathgroup4 -LaTeX Font Info: Overwriting symbol font `mincho' in version `bold' -(Font) JY1/mc/m/n --> JY1/gt/m/n on input line 541. -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 9.60999pt on input line 732. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 9.60999pt on input line 732. -\fullwidth=\dimen120 -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 7.68799pt on input line 871. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 7.68799pt on input line 871. -\c@part=\count83 -\c@chapter=\count84 -\c@section=\count85 -\c@subsection=\count86 -\c@subsubsection=\count87 -\c@paragraph=\count88 -\c@subparagraph=\count89 -\@abstractbox=\box43 -\c@figure=\count90 -\c@table=\count91 -\abovecaptionskip=\skip42 -\belowcaptionskip=\skip43 -\jsc@tocl@width=\dimen121 -\@lnumwidth=\dimen122 -\bibindent=\dimen123 -(/usr/local/texlive/2019/texmf-dist/tex/platex/jsclasses/jslogo.sty -Package: jslogo 2017/02/24 okumura, texjporg -LaTeX Info: Redefining \TeX on input line 94. -LaTeX Info: Redefining \LaTeX on input line 147. -LaTeX Info: Redefining \LaTeXe on input line 200. -) -\heisei=\count92 -) -(./ie-thesis.sty -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/graphicx.sty -Package: graphicx 2017/06/01 v1.1a Enhanced LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/keyval.sty -Package: keyval 2014/10/28 v1.15 key=value parser (DPC) -\KV@toks@=\toks15 -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/graphics.sty -Package: graphics 2017/06/25 v1.2c Standard LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/trig.sty -Package: trig 2016/01/03 v1.10 sin cos tan (DPC) -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics-cfg/graphics.cfg -File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration -) -Package graphics Info: Driver file: dvips.def on input line 99. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics-def/dvips.def -File: dvips.def 2017/06/20 v3.1d Graphics/color driver for dvips -)) -\Gin@req@height=\dimen124 -\Gin@req@width=\dimen125 -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/color.sty -Package: color 2016/07/10 v1.1e Standard LaTeX Color (DPC) - -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics-cfg/color.cfg -File: color.cfg 2016/01/02 v1.6 sample color configuration -) -Package color Info: Driver file: dvipdfmx.def on input line 147. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics-def/dvipdfmx.def -File: dvipdfmx.def 2017/06/24 v5.0g Graphics/color driver for dvipdfmx -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/graphics/dvipsnam.def -File: dvipsnam.def 2016/06/17 v3.0m Driver-dependent file (DPC,SPQR) -)) -(/usr/local/texlive/2019/texmf-dist/tex/latex/setspace/setspace.sty -Package: setspace 2011/12/19 v6.7a set line spacing -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/url/url.sty -\Urlmuskip=\muskip10 -Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/amsmath/amsmath.sty -Package: amsmath 2018/12/01 v2.17b AMS math features -\@mathmargin=\skip44 - -For additional information on amsmath, use the `?' option. -(/usr/local/texlive/2019/texmf-dist/tex/latex/amsmath/amstext.sty -Package: amstext 2000/06/29 v2.01 AMS text - -(/usr/local/texlive/2019/texmf-dist/tex/latex/amsmath/amsgen.sty -File: amsgen.sty 1999/11/30 v2.0 generic functions -\@emptytoks=\toks16 -\ex@=\dimen126 -)) -(/usr/local/texlive/2019/texmf-dist/tex/latex/amsmath/amsbsy.sty -Package: amsbsy 1999/11/29 v1.2d Bold Symbols -\pmbraise@=\dimen127 -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/amsmath/amsopn.sty -Package: amsopn 2016/03/08 v2.02 operator names -) -\inf@bad=\count93 -LaTeX Info: Redefining \frac on input line 223. -\uproot@=\count94 -\leftroot@=\count95 -LaTeX Info: Redefining \overline on input line 385. -\classnum@=\count96 -\DOTSCASE@=\count97 -LaTeX Info: Redefining \ldots on input line 482. -LaTeX Info: Redefining \dots on input line 485. -LaTeX Info: Redefining \cdots on input line 606. -\Mathstrutbox@=\box44 -\strutbox@=\box45 -\big@size=\dimen128 -LaTeX Font Info: Redeclaring font encoding OML on input line 729. -LaTeX Font Info: Redeclaring font encoding OMS on input line 730. -\macc@depth=\count98 -\c@MaxMatrixCols=\count99 -\dotsspace@=\muskip11 -\c@parentequation=\count100 -\dspbrk@lvl=\count101 -\tag@help=\toks17 -\row@=\count102 -\column@=\count103 -\maxfields@=\count104 -\andhelp@=\toks18 -\eqnshift@=\dimen129 -\alignsep@=\dimen130 -\tagshift@=\dimen131 -\tagwidth@=\dimen132 -\totwidth@=\dimen133 -\lineht@=\dimen134 -\@envbody=\toks19 -\multlinegap=\skip45 -\multlinetaggap=\skip46 -\mathdisplay@stack=\toks20 -LaTeX Info: Redefining \[ on input line 2844. -LaTeX Info: Redefining \] on input line 2845. -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty -Package: fancyhdr 2019/01/31 v3.10 Extensive control of page headers and footer -s -\f@nch@headwidth=\skip47 -\f@nch@O@elh=\skip48 -\f@nch@O@erh=\skip49 -\f@nch@O@olh=\skip50 -\f@nch@O@orh=\skip51 -\f@nch@O@elf=\skip52 -\f@nch@O@erf=\skip53 -\f@nch@O@olf=\skip54 -\f@nch@O@orf=\skip55 -)) -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/txfonts.sty -Package: txfonts 2008/01/22 v3.2.1 -LaTeX Font Info: Redeclaring symbol font `operators' on input line 21. -LaTeX Font Info: Overwriting symbol font `operators' in version `normal' -(Font) OT1/cmr/m/n --> OT1/txr/m/n on input line 21. -LaTeX Font Info: Overwriting symbol font `operators' in version `bold' -(Font) OT1/cmr/bx/n --> OT1/txr/m/n on input line 21. -LaTeX Font Info: Overwriting symbol font `operators' in version `bold' -(Font) OT1/txr/m/n --> OT1/txr/bx/n on input line 22. -\symitalic=\mathgroup5 -LaTeX Font Info: Overwriting symbol font `italic' in version `bold' -(Font) OT1/txr/m/it --> OT1/txr/bx/it on input line 26. -LaTeX Font Info: Redeclaring math alphabet \mathbf on input line 29. -LaTeX Font Info: Overwriting math alphabet `\mathbf' in version `normal' -(Font) OT1/cmr/bx/n --> OT1/txr/bx/n on input line 29. -LaTeX Font Info: Overwriting math alphabet `\mathbf' in version `bold' -(Font) OT1/cmr/bx/n --> OT1/txr/bx/n on input line 29. -LaTeX Font Info: Redeclaring math alphabet \mathit on input line 30. -LaTeX Font Info: Overwriting math alphabet `\mathit' in version `normal' -(Font) OT1/cmr/m/it --> OT1/txr/m/it on input line 30. -LaTeX Font Info: Overwriting math alphabet `\mathit' in version `bold' -(Font) OT1/cmr/bx/it --> OT1/txr/m/it on input line 30. -LaTeX Font Info: Overwriting math alphabet `\mathit' in version `bold' -(Font) OT1/txr/m/it --> OT1/txr/bx/it on input line 31. -LaTeX Font Info: Redeclaring math alphabet \mathsf on input line 40. -LaTeX Font Info: Overwriting math alphabet `\mathsf' in version `normal' -(Font) OT1/cmss/m/n --> OT1/txss/m/n on input line 40. -LaTeX Font Info: Overwriting math alphabet `\mathsf' in version `bold' -(Font) OT1/cmss/bx/n --> OT1/txss/m/n on input line 40. -LaTeX Font Info: Overwriting math alphabet `\mathsf' in version `bold' -(Font) OT1/txss/m/n --> OT1/txss/b/n on input line 41. -LaTeX Font Info: Redeclaring math alphabet \mathtt on input line 50. -LaTeX Font Info: Overwriting math alphabet `\mathtt' in version `normal' -(Font) OT1/cmtt/m/n --> OT1/txtt/m/n on input line 50. -LaTeX Font Info: Overwriting math alphabet `\mathtt' in version `bold' -(Font) OT1/cmtt/m/n --> OT1/txtt/m/n on input line 50. -LaTeX Font Info: Overwriting math alphabet `\mathtt' in version `bold' -(Font) OT1/txtt/m/n --> OT1/txtt/b/n on input line 51. -LaTeX Font Info: Redeclaring symbol font `letters' on input line 58. -LaTeX Font Info: Overwriting symbol font `letters' in version `normal' -(Font) OML/cmm/m/it --> OML/txmi/m/it on input line 58. -LaTeX Font Info: Overwriting symbol font `letters' in version `bold' -(Font) OML/cmm/b/it --> OML/txmi/m/it on input line 58. -LaTeX Font Info: Overwriting symbol font `letters' in version `bold' -(Font) OML/txmi/m/it --> OML/txmi/bx/it on input line 59. -\symlettersA=\mathgroup6 -LaTeX Font Info: Overwriting symbol font `lettersA' in version `bold' -(Font) U/txmia/m/it --> U/txmia/bx/it on input line 67. -LaTeX Font Info: Redeclaring symbol font `symbols' on input line 77. -LaTeX Font Info: Overwriting symbol font `symbols' in version `normal' -(Font) OMS/cmsy/m/n --> OMS/txsy/m/n on input line 77. -LaTeX Font Info: Overwriting symbol font `symbols' in version `bold' -(Font) OMS/cmsy/b/n --> OMS/txsy/m/n on input line 77. -LaTeX Font Info: Overwriting symbol font `symbols' in version `bold' -(Font) OMS/txsy/m/n --> OMS/txsy/bx/n on input line 78. -\symAMSa=\mathgroup7 -LaTeX Font Info: Overwriting symbol font `AMSa' in version `bold' -(Font) U/txsya/m/n --> U/txsya/bx/n on input line 94. -\symAMSb=\mathgroup8 -LaTeX Font Info: Overwriting symbol font `AMSb' in version `bold' -(Font) U/txsyb/m/n --> U/txsyb/bx/n on input line 103. -\symsymbolsC=\mathgroup9 -LaTeX Font Info: Overwriting symbol font `symbolsC' in version `bold' -(Font) U/txsyc/m/n --> U/txsyc/bx/n on input line 113. -LaTeX Font Info: Redeclaring symbol font `largesymbols' on input line 120. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `normal' -(Font) OMX/cmex/m/n --> OMX/txex/m/n on input line 120. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold' -(Font) OMX/cmex/m/n --> OMX/txex/m/n on input line 120. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold' -(Font) OMX/txex/m/n --> OMX/txex/bx/n on input line 121. -\symlargesymbolsA=\mathgroup10 -LaTeX Font Info: Overwriting symbol font `largesymbolsA' in version `bold' -(Font) U/txexa/m/n --> U/txexa/bx/n on input line 129. -LaTeX Info: Redefining \not on input line 1043. -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/listings/listings.sty -\lst@mode=\count105 -\lst@gtempboxa=\box46 -\lst@token=\toks21 -\lst@length=\count106 -\lst@currlwidth=\dimen135 -\lst@column=\count107 -\lst@pos=\count108 -\lst@lostspace=\dimen136 -\lst@width=\dimen137 -\lst@newlines=\count109 -\lst@lineno=\count110 -\lst@maxwidth=\dimen138 - -(/usr/local/texlive/2019/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2019/02/27 1.8b (Carsten Heinz) -\c@lstnumber=\count111 -\lst@skipnumbers=\count112 -\lst@framebox=\box47 -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/listings/listings.cfg -File: listings.cfg 2019/02/27 1.8b listings configuration -)) -Package: listings 2019/02/27 1.8b (Carsten Heinz) - -(./jlisting.sty -Package: jlisting 2006/02/20 0.2 (Thor) -\lst@nextchar=\count113 -\lst@inputfile=\read1 -) -(/usr/local/texlive/2019/texmf-dist/tex/latex/mnsymbol/MnSymbol.sty -Package: MnSymbol 2007/01/21 v1.4 support for the MnSymbol font - -(/usr/local/texlive/2019/texmf-dist/tex/latex/base/textcomp.sty -Package: textcomp 2018/08/11 v2.0j Standard LaTeX package -Package textcomp Info: Sub-encoding information: -(textcomp) 5 = only ISO-Adobe without \textcurrency -(textcomp) 4 = 5 + \texteuro -(textcomp) 3 = 4 + \textohm -(textcomp) 2 = 3 + \textestimated + \textcurrency -(textcomp) 1 = TS1 - \textcircled - \t -(textcomp) 0 = TS1 (full) -(textcomp) Font families with sub-encoding setting implement -(textcomp) only a restricted character set as indicated. -(textcomp) Family '?' is the default used for unknown fonts. -(textcomp) See the documentation for details. -Package textcomp Info: Setting ? sub-encoding to TS1/1 on input line 79. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/base/ts1enc.def -File: ts1enc.def 2001/06/05 v3.0e (jk/car/fm) Standard LaTeX file -Now handling font encoding TS1 ... -... processing UTF-8 mapping file for font encoding TS1 - -(/usr/local/texlive/2019/texmf-dist/tex/latex/base/ts1enc.dfu -File: ts1enc.dfu 2018/10/05 v1.2f UTF-8 support for inputenc - defining Unicode char U+00A2 (decimal 162) - defining Unicode char U+00A3 (decimal 163) - defining Unicode char U+00A4 (decimal 164) - defining Unicode char U+00A5 (decimal 165) - defining Unicode char U+00A6 (decimal 166) - defining Unicode char U+00A7 (decimal 167) - defining Unicode char U+00A8 (decimal 168) - defining Unicode char U+00A9 (decimal 169) - defining Unicode char U+00AA (decimal 170) - defining Unicode char U+00AC (decimal 172) - defining Unicode char U+00AE (decimal 174) - defining Unicode char U+00AF (decimal 175) - defining Unicode char U+00B0 (decimal 176) - defining Unicode char U+00B1 (decimal 177) - defining Unicode char U+00B2 (decimal 178) - defining Unicode char U+00B3 (decimal 179) - defining Unicode char U+00B4 (decimal 180) - defining Unicode char U+00B5 (decimal 181) - defining Unicode char U+00B6 (decimal 182) - defining Unicode char U+00B7 (decimal 183) - defining Unicode char U+00B9 (decimal 185) - defining Unicode char U+00BA (decimal 186) - defining Unicode char U+00BC (decimal 188) - defining Unicode char U+00BD (decimal 189) - defining Unicode char U+00BE (decimal 190) - defining Unicode char U+00D7 (decimal 215) - defining Unicode char U+00F7 (decimal 247) - defining Unicode char U+0192 (decimal 402) - defining Unicode char U+02C7 (decimal 711) - defining Unicode char U+02D8 (decimal 728) - defining Unicode char U+02DD (decimal 733) - defining Unicode char U+0E3F (decimal 3647) - defining Unicode char U+2016 (decimal 8214) - defining Unicode char U+2020 (decimal 8224) - defining Unicode char U+2021 (decimal 8225) - defining Unicode char U+2022 (decimal 8226) - defining Unicode char U+2030 (decimal 8240) - defining Unicode char U+2031 (decimal 8241) - defining Unicode char U+203B (decimal 8251) - defining Unicode char U+203D (decimal 8253) - defining Unicode char U+2044 (decimal 8260) - defining Unicode char U+204E (decimal 8270) - defining Unicode char U+2052 (decimal 8274) - defining Unicode char U+20A1 (decimal 8353) - defining Unicode char U+20A4 (decimal 8356) - defining Unicode char U+20A6 (decimal 8358) - defining Unicode char U+20A9 (decimal 8361) - defining Unicode char U+20AB (decimal 8363) - defining Unicode char U+20AC (decimal 8364) - defining Unicode char U+20B1 (decimal 8369) - defining Unicode char U+2103 (decimal 8451) - defining Unicode char U+2116 (decimal 8470) - defining Unicode char U+2117 (decimal 8471) - defining Unicode char U+211E (decimal 8478) - defining Unicode char U+2120 (decimal 8480) - defining Unicode char U+2122 (decimal 8482) - defining Unicode char U+2126 (decimal 8486) - defining Unicode char U+2127 (decimal 8487) - defining Unicode char U+212E (decimal 8494) - defining Unicode char U+2190 (decimal 8592) - defining Unicode char U+2191 (decimal 8593) - defining Unicode char U+2192 (decimal 8594) - defining Unicode char U+2193 (decimal 8595) - defining Unicode char U+2329 (decimal 9001) - defining Unicode char U+232A (decimal 9002) - defining Unicode char U+2422 (decimal 9250) - defining Unicode char U+25E6 (decimal 9702) - defining Unicode char U+25EF (decimal 9711) - defining Unicode char U+266A (decimal 9834) - defining Unicode char U+FEFF (decimal 65279) -)) -LaTeX Info: Redefining \oldstylenums on input line 334. -Package textcomp Info: Setting cmr sub-encoding to TS1/0 on input line 349. -Package textcomp Info: Setting cmss sub-encoding to TS1/0 on input line 350. -Package textcomp Info: Setting cmtt sub-encoding to TS1/0 on input line 351. -Package textcomp Info: Setting cmvtt sub-encoding to TS1/0 on input line 352. -Package textcomp Info: Setting cmbr sub-encoding to TS1/0 on input line 353. -Package textcomp Info: Setting cmtl sub-encoding to TS1/0 on input line 354. -Package textcomp Info: Setting ccr sub-encoding to TS1/0 on input line 355. -Package textcomp Info: Setting ptm sub-encoding to TS1/4 on input line 356. -Package textcomp Info: Setting pcr sub-encoding to TS1/4 on input line 357. -Package textcomp Info: Setting phv sub-encoding to TS1/4 on input line 358. -Package textcomp Info: Setting ppl sub-encoding to TS1/3 on input line 359. -Package textcomp Info: Setting pag sub-encoding to TS1/4 on input line 360. -Package textcomp Info: Setting pbk sub-encoding to TS1/4 on input line 361. -Package textcomp Info: Setting pnc sub-encoding to TS1/4 on input line 362. -Package textcomp Info: Setting pzc sub-encoding to TS1/4 on input line 363. -Package textcomp Info: Setting bch sub-encoding to TS1/4 on input line 364. -Package textcomp Info: Setting put sub-encoding to TS1/5 on input line 365. -Package textcomp Info: Setting uag sub-encoding to TS1/5 on input line 366. -Package textcomp Info: Setting ugq sub-encoding to TS1/5 on input line 367. -Package textcomp Info: Setting ul8 sub-encoding to TS1/4 on input line 368. -Package textcomp Info: Setting ul9 sub-encoding to TS1/4 on input line 369. -Package textcomp Info: Setting augie sub-encoding to TS1/5 on input line 370. -Package textcomp Info: Setting dayrom sub-encoding to TS1/3 on input line 371. -Package textcomp Info: Setting dayroms sub-encoding to TS1/3 on input line 372. - -Package textcomp Info: Setting pxr sub-encoding to TS1/0 on input line 373. -Package textcomp Info: Setting pxss sub-encoding to TS1/0 on input line 374. -Package textcomp Info: Setting pxtt sub-encoding to TS1/0 on input line 375. -Package textcomp Info: Setting txr sub-encoding to TS1/0 on input line 376. -Package textcomp Info: Setting txss sub-encoding to TS1/0 on input line 377. -Package textcomp Info: Setting txtt sub-encoding to TS1/0 on input line 378. -Package textcomp Info: Setting lmr sub-encoding to TS1/0 on input line 379. -Package textcomp Info: Setting lmdh sub-encoding to TS1/0 on input line 380. -Package textcomp Info: Setting lmss sub-encoding to TS1/0 on input line 381. -Package textcomp Info: Setting lmssq sub-encoding to TS1/0 on input line 382. -Package textcomp Info: Setting lmvtt sub-encoding to TS1/0 on input line 383. -Package textcomp Info: Setting lmtt sub-encoding to TS1/0 on input line 384. -Package textcomp Info: Setting qhv sub-encoding to TS1/0 on input line 385. -Package textcomp Info: Setting qag sub-encoding to TS1/0 on input line 386. -Package textcomp Info: Setting qbk sub-encoding to TS1/0 on input line 387. -Package textcomp Info: Setting qcr sub-encoding to TS1/0 on input line 388. -Package textcomp Info: Setting qcs sub-encoding to TS1/0 on input line 389. -Package textcomp Info: Setting qpl sub-encoding to TS1/0 on input line 390. -Package textcomp Info: Setting qtm sub-encoding to TS1/0 on input line 391. -Package textcomp Info: Setting qzc sub-encoding to TS1/0 on input line 392. -Package textcomp Info: Setting qhvc sub-encoding to TS1/0 on input line 393. -Package textcomp Info: Setting futs sub-encoding to TS1/4 on input line 394. -Package textcomp Info: Setting futx sub-encoding to TS1/4 on input line 395. -Package textcomp Info: Setting futj sub-encoding to TS1/4 on input line 396. -Package textcomp Info: Setting hlh sub-encoding to TS1/3 on input line 397. -Package textcomp Info: Setting hls sub-encoding to TS1/3 on input line 398. -Package textcomp Info: Setting hlst sub-encoding to TS1/3 on input line 399. -Package textcomp Info: Setting hlct sub-encoding to TS1/5 on input line 400. -Package textcomp Info: Setting hlx sub-encoding to TS1/5 on input line 401. -Package textcomp Info: Setting hlce sub-encoding to TS1/5 on input line 402. -Package textcomp Info: Setting hlcn sub-encoding to TS1/5 on input line 403. -Package textcomp Info: Setting hlcw sub-encoding to TS1/5 on input line 404. -Package textcomp Info: Setting hlcf sub-encoding to TS1/5 on input line 405. -Package textcomp Info: Setting pplx sub-encoding to TS1/3 on input line 406. -Package textcomp Info: Setting pplj sub-encoding to TS1/3 on input line 407. -Package textcomp Info: Setting ptmx sub-encoding to TS1/4 on input line 408. -Package textcomp Info: Setting ptmj sub-encoding to TS1/4 on input line 409. -) -LaTeX Info: Redefining \dagger on input line 84. -LaTeX Info: Redefining \ddagger on input line 84. -LaTeX Info: Redefining \mathparagraph on input line 84. -LaTeX Info: Redefining \mathsection on input line 84. -LaTeX Info: Redefining \mathdollar on input line 84. -LaTeX Info: Redefining \mathsterling on input line 84. -LaTeX Info: Redefining \circledS on input line 84. -LaTeX Info: Redefining \Re on input line 84. -LaTeX Info: Redefining \Im on input line 84. -LaTeX Info: Redefining \dotplus on input line 84. -LaTeX Info: Redefining \thicksim on input line 84. -LaTeX Info: Redefining \thickapprox on input line 84. -LaTeX Info: Redefining \veebar on input line 84. -LaTeX Info: Redefining \barwedge on input line 84. -LaTeX Info: Redefining \doublebarwedge on input line 84. -LaTeX Info: Redefining \centerdot on input line 84. -LaTeX Info: Redefining \divideontimes on input line 84. -\symMnSyA=\mathgroup11 -\symMnSyB=\mathgroup12 -\symMnSyC=\mathgroup13 -\symMnSyD=\mathgroup14 -LaTeX Font Info: Redeclaring symbol font `largesymbols' on input line 119. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `normal' -(Font) OMX/txex/m/n --> OMX/MnSymbolE/m/n on input line 119. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold' -(Font) OMX/txex/bx/n --> OMX/MnSymbolE/m/n on input line 119. -LaTeX Font Info: Redeclaring symbol font `symbols' on input line 120. -LaTeX Font Info: Encoding `OMS' has changed to `U' for symbol font -(Font) `symbols' in the math version `normal' on input line 120. -LaTeX Font Info: Overwriting symbol font `symbols' in version `normal' -(Font) OMS/txsy/m/n --> U/MnSymbolF/m/n on input line 120. -LaTeX Font Info: Encoding `OMS' has changed to `U' for symbol font -(Font) `symbols' in the math version `bold' on input line 120. -LaTeX Font Info: Overwriting symbol font `symbols' in version `bold' -(Font) OMS/txsy/bx/n --> U/MnSymbolF/m/n on input line 120. -LaTeX Font Info: Overwriting symbol font `MnSyA' in version `bold' -(Font) U/MnSymbolA/m/n --> U/MnSymbolA/b/n on input line 121. -LaTeX Font Info: Overwriting symbol font `MnSyB' in version `bold' -(Font) U/MnSymbolB/m/n --> U/MnSymbolB/b/n on input line 122. -LaTeX Font Info: Overwriting symbol font `MnSyC' in version `bold' -(Font) U/MnSymbolC/m/n --> U/MnSymbolC/b/n on input line 123. -LaTeX Font Info: Overwriting symbol font `MnSyD' in version `bold' -(Font) U/MnSymbolD/m/n --> U/MnSymbolD/b/n on input line 124. -LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold' -(Font) OMX/MnSymbolE/m/n --> OMX/MnSymbolE/b/n on input line 1 -25. -LaTeX Font Info: Overwriting symbol font `symbols' in version `bold' -(Font) U/MnSymbolF/m/n --> U/MnSymbolF/b/n on input line 126. -LaTeX Font Info: Redeclaring math alphabet \mathcal on input line 241. -LaTeX Font Info: Overwriting math alphabet `\mathcal' in version `bold' -(Font) OMS/MnSymbolS/m/n --> OMS/MnSymbolS/b/n on input line 2 -41. -LaTeX Info: Redefining \longrightarrow on input line 548. -LaTeX Info: Redefining \longleftarrow on input line 549. -LaTeX Info: Redefining \longleftrightarrow on input line 550. -LaTeX Info: Redefining \Longrightarrow on input line 551. -LaTeX Info: Redefining \Longleftarrow on input line 552. -LaTeX Info: Redefining \Longleftrightarrow on input line 553. -LaTeX Info: Redefining \longmapsto on input line 554. -LaTeX Info: Redefining \vdots on input line 868. -LaTeX Info: Redefining \coloneq on input line 1445. -LaTeX Font Info: Redeclaring math symbol \braceld on input line 1721. -LaTeX Font Info: Redeclaring math symbol \bracelu on input line 1722. -LaTeX Font Info: Redeclaring math symbol \bracerd on input line 1723. -LaTeX Font Info: Redeclaring math symbol \braceru on input line 1724. -LaTeX Info: Redefining \downbracefill on input line 1799. -LaTeX Info: Redefining \upbracefill on input line 1800. -LaTeX Info: Redefining \overbrace on input line 1819. -LaTeX Info: Redefining \underbrace on input line 1820. -LaTeX Info: Redefining \surd on input line 1843. -LaTeX Font Info: Redeclaring math accent \widehat on input line 1845. -LaTeX Font Info: Redeclaring math accent \widetilde on input line 1846. -LaTeX Font Info: Redeclaring math accent \vec on input line 1848. -) -\symMnLargeSymbols=\mathgroup15 -LaTeX Font Info: Overwriting symbol font `MnLargeSymbols' in version `bold' -(Font) OMX/MnSymbolE/m/n --> OMX/MnSymbolE/b/n on input line 2 -9. - - -LaTeX Warning: Unused global option(s): - [title]. - -(./thesis.aux (./text/introduction.aux) (./text/chapter2.aux) -(./text/chapter3.aux) (./text/chapter4.aux) (./text/chapter5.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. -LaTeX Font Info: Try loading font information for OML+txmi on input line 72. - - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/omltxmi.fd -File: omltxmi.fd 2000/12/15 v3.1 -) -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 72. -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 72. -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for OMS/txsy/m/n on input line 72. -LaTeX Font Info: Try loading font information for OMS+txsy on input line 72. - - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/omstxsy.fd -File: omstxsy.fd 2000/12/15 v3.1 -) -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for OMX/txex/m/n on input line 72. -LaTeX Font Info: Try loading font information for OMX+txex on input line 72. - - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/omxtxex.fd -File: omxtxex.fd 2000/12/15 v3.1 -) -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for U/txexa/m/n on input line 72. -LaTeX Font Info: Try loading font information for U+txexa on input line 72. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/utxexa.fd -File: utxexa.fd 2000/12/15 v3.1 -) -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 72. -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 72. -LaTeX Font Info: ... okay on input line 72. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 72. -LaTeX Font Info: Try loading font information for TS1+cmr on input line 72. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/base/ts1cmr.fd -File: ts1cmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: ... okay on input line 72. - -(I search kanjifont definition file: . . ) (I search font definition file: . . -. . . . . . ) -LaTeX Font Info: Try loading font information for OT1+txr on input line 72. - (/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/ot1txr.fd -File: ot1txr.fd 2000/12/15 v3.1 -) -\c@lstlisting=\count114 -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 6.72699pt on input line 73. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 4.805pt on input line 73. -LaTeX Font Info: Try loading font information for U+txmia on input line 73. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/utxmia.fd -File: utxmia.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Try loading font information for U+txsya on input line 73. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/utxsya.fd -File: utxsya.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Try loading font information for U+txsyb on input line 73. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/utxsyb.fd -File: utxsyb.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Try loading font information for U+txsyc on input line 73. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/utxsyc.fd -File: utxsyc.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <10> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 9.60999pt on input line 73. -LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <10> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 9.60999pt on input line 73. -LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 13.83836pt on input line 73. -LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 13.83836pt on input line 73. -LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <17.28> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 16.60605pt on input line 73. -LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <17.28> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 73. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 16.60605pt on input line 73. -File: logo_u-ryukyu.jpg Graphic file (type bmp) - - [1 - -] -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 11.53198pt on input line 73. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 11.53198pt on input line 73. - -(./text/Jabstract.tex) [2] (./text/Eabstract.tex) -LaTeX Font Info: Try loading font information for OT1+txss on input line 76. - - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/ot1txss.fd -File: ot1txss.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Font shape `OT1/txss/m/n' will be -(Font) scaled to size 9.49997pt on input line 76. - [3] -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 23.90964pt on input line 76. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 23.90964pt on input line 76. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 23.90964pt on input line 76. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 23.90964pt on input line 76. -LaTeX Font Info: Font shape `OT1/txss/m/n' will be -(Font) scaled to size 23.63593pt on input line 76. - -(./thesis.toc [4 - -]) -\tf@toc=\write3 -\openout3 = `thesis.toc'. - - [5] (./thesis.lof) -\tf@lof=\write4 -\openout4 = `thesis.lof'. - - [6 - -] (./thesis.lot) -\tf@lot=\write5 -\openout5 = `thesis.lot'. - - [7 - -] (./thesis.lol) -\tf@lol=\write6 -\openout6 = `thesis.lol'. - - -[0 - -] -\openout2 = `./text/introduction.aux'. - - (./text/introduction.tex -第1章 -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 19.9311pt on input line 1. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 19.9311pt on input line 1. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 19.9311pt on input line 1. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 19.9311pt on input line 1. -LaTeX Font Info: Font shape `OT1/txss/m/n' will be -(Font) scaled to size 19.70294pt on input line 1. -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 13.83836pt on input line 3. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 13.83836pt on input line 3. -LaTeX Font Info: Font shape `OT1/txss/m/n' will be -(Font) scaled to size 13.67995pt on input line 3. -) [1 - - -] [2] -\openout2 = `./text/chapter2.aux'. - - (./text/chapter2.tex -第2章 -[3 - - - -] -File: ./figs/BinarySearchTree.png Graphic file (type bmp) -<./figs/BinarySearchTree.png> -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 8.64899pt on input line 26. -LaTeX Font Info: Font shape `JY1/mc/m/n' will be -(Font) scaled to size 8.64899pt on input line 26. - [4] -File: ./figs/RedBlackTree.png Graphic file (type bmp) -<./figs/RedBlackTree.png> - - -! LaTeX Error: File `../../Report.tex' not found. - -Type X to quit or to proceed, -or enter new name. (Default extension: tex) - -Enter file name: -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 11.53198pt on input line 58. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 11.53198pt on input line 58. -LaTeX Font Info: Font shape `OT1/txss/m/n' will be -(Font) scaled to size 11.39996pt on input line 58. -[5] -LaTeX Font Info: Try loading font information for OT1+txtt on input line 61. - - (/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/ot1txtt.fd -File: ot1txtt.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 6.72699pt on input line 62. -LaTeX Font Info: Font shape `JT1/gt/m/n' will be -(Font) scaled to size 8.64899pt on input line 62. -LaTeX Font Info: Font shape `JY1/gt/m/n' will be -(Font) scaled to size 8.64899pt on input line 62. - [6] -LaTeX Font Info: Font shape `JT1/mc/m/n' will be -(Font) scaled to size 4.805pt on input line 102. - -[7] - -LaTeX Warning: Command \textless invalid in math mode on input line 118. - -LaTeX Font Info: Try loading font information for OML+txr on input line 118. - -(/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/omltxr.fd -File: omltxr.fd 2000/12/15 v3.1 -) -LaTeX Font Info: Font shape `OML/txr/m/n' in size <10> not available -(Font) Font shape `OML/txmi/m/it' tried instead on input line 118. - - - -LaTeX Warning: Command \textless invalid in math mode on input line 118. - - -LaTeX Warning: Command \textless invalid in math mode on input line 120. - - -LaTeX Warning: Command \textless invalid in math mode on input line 120. - - -LaTeX Warning: Command \textgreater invalid in math mode on input line 120. - - -LaTeX Warning: Command \textgreater invalid in math mode on input line 120. - - -LaTeX Warning: Command \textless invalid in math mode on input line 122. - - -LaTeX Warning: Command \textless invalid in math mode on input line 122. - - -LaTeX Warning: Command \textgreater invalid in math mode on input line 126. - - -LaTeX Warning: Command \textgreater invalid in math mode on input line 126. - -[8] [9]) [10] -\openout2 = `./text/chapter3.aux'. - - (./text/chapter3.tex -第3章 -) [11 - - - -] -\openout2 = `./text/chapter4.aux'. - - (./text/chapter4.tex -第4章 -[12 - - - -] [13] [14] - -LaTeX Warning: Command \textless invalid in math mode on input line 98. - - -LaTeX Warning: Command \textless invalid in math mode on input line 98. - -[15] [16]) [17] -\openout2 = `./text/chapter5.aux'. - - (./text/chapter5.tex -第5章 -[18 - - - -] - -LaTeX Warning: Command \textless invalid in math mode on input line 28. - - -LaTeX Warning: Command \textless invalid in math mode on input line 28. - -[19 - -<<<<<<< HEAD -] [20] [21] [22 -======= -] [20] -Overfull \hbox (87.32846pt too wide) in paragraph at lines 89--102 - [][][][] - [] - -[21] -LaTeX Font Info: Try loading font information for TS1+txtt on input line 117 -. - (/usr/local/texlive/2019/texmf-dist/tex/latex/txfonts/ts1txtt.fd -File: ts1txtt.fd 2000/12/15 v3.1 -) [22 ->>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4 - -] -[23] [24]) [25] -\openout2 = `./text/chapter6.aux'. - - (./text/chapter6.tex -第6章 -[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 - - -] -\openout2 = `./text/reference.aux'. - - (./text/reference.tex -Underfull \hbox (badness 10000) in paragraph at lines 2--5 -[]\OT1/txr/m/n/10 Hoare logic - \JY1/mc/m/n/10 並列信頼研 \OT1/txr/m/n/10 mer-c -u-rial repos-i-tory, http://www. cr.ie.u- - [] - -) [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. - - ) -Here is how much of TeX's memory you used: - 6124 strings out of 493223 - 79282 string characters out of 6144415 - 236219 words of memory out of 5000000 - 9946 multiletter control sequences out of 15000+600000 - 35078 words of font info for 122 fonts, out of 8000000 for 9000 - 934 hyphenation exceptions out of 8191 - 36i,12n,45p,675b,1839s stack positions out of 5000i,500n,10000p,200000b,80000s - -Output written on thesis.dvi (36 pages, 121092 bytes). ->>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4 diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.lol --- a/Report/final/thesis.lol Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -\contentsline {lstlisting}{\numberline {2.1}AgdaにおけるData型の実装}{6}% -\contentsline {lstlisting}{\numberline {2.2}Agdaにおける足し算の実装}{6}% -\contentsline {lstlisting}{\numberline {2.3}Agdにおける二項演算子の実装}{7}% -\contentsline {lstlisting}{\numberline {2.4}Agdaにおける場合分けの書き方}{7}% -\contentsline {lstlisting}{\numberline {2.5}GearsAgdaにおける足し算の実装}{9}% -\contentsline {lstlisting}{\numberline {4.1}BinarySearchTreeの基本的な実装}{12}% -\contentsline {lstlisting}{\numberline {4.2}RedBlackTreeの基本的な実装}{13}% -\contentsline {lstlisting}{\numberline {4.3}RBtreeInvariantの実装}{14}% -\contentsline {lstlisting}{\numberline {4.4}stackInvariantの実装}{16}% -\contentsline {lstlisting}{\numberline {5.1}findRBTの実装}{19}% -\contentsline {lstlisting}{\numberline {5.2}findTestの実装}{22}% -\contentsline {lstlisting}{\numberline {5.3}Keyの値14のfindTest実行結果}{23}% -\contentsline {lstlisting}{\numberline {5.4}Keyの値1のfindTest実行結果}{24}% diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.lot --- a/Report/final/thesis.lot Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } -\contentsline {table}{\numberline {5.1}{\ignorespaces findRBTに使用される関数}}{19}% -\contentsline {table}{\numberline {5.2}{\ignorespaces findTestに使用される関数}}{21}% -\addvspace {10\jsc@mpt } -\addvspace {10\jsc@mpt } diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.synctex.gz Binary file Report/final/thesis.synctex.gz has changed diff -r 70346fe80c78 -r dd37dd73a8ea Report/final/thesis.toc --- a/Report/final/thesis.toc Thu Feb 08 15:46:29 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -<<<<<<< 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}% -\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章}まとめと今後の展望}{26}% -\contentsline {chapter}{参考文献}{28}% ->>>>>>> 12c8ba943caeb23958ca18de47a5d51a88752ad4