\relax 
\bibstyle{cpsnamedwithapalikesorting}
\citation{grundlagen-first-edition-volume-one}
\citation{grundlagen-first-edition-volume-one}
\citation{grundlagen-first-edition-volume-two}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-second-edition-volume-two}
\citation{grundlagen-first-edition-volume-two}
\citation{grundlagen-second-edition-volume-two}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}The Explicit Historical Source of the Problem}{2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Subject Matter}{3}}
\citation{grundlagen-first-edition-volume-two}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-german-english-edition-volume-one-two}
\citation{grundlagen-first-edition-volume-two}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}A Lacuna in Hilbert--\unhbox \voidb@x \hbox {Ber\discretionary {-}{}{}nay\unprotectedes }?}{4}}
\newlabel{section A Lacuna in}{{1.3}{4}}
\citation{middeldorp_goodstein}
\citation{ackermann-1925}
\citation{unendliche}
\citation{unendliche}
\citation{grundlagenvortrag}
\citation{klopdiss}
\citation{klopCRS1993}
\citation{nipkowLICS1991}
\citation{Raamsdonk99}
\citation{JouannaudOkadaLICS1991}
\citation{wirth-jsc}
\citation{klopCRS1993}
\citation{klopdiss}
\citation{klopCRS1993}
\citation{klopdiss}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Alternative Proofs by Applying Theories of First- or Higher-Order Rewriting?}{5}}
\citation{klopdiss}
\citation{klopCRS1993}
\citation{klopCRS1993}
\citation{klopdiss}
\citation{Raamsdonk01}
\citation{raamsdonktermination}
\citation{klopdiss}
\citation{tait-termination-simply-typed}
\citation{tait-termination-simply-typed}
\citation{writing-mathematics}
\citation{klopdiss}
\citation{Moore_Wirth_Automation_of_Mathematical_Induction_2013}
\@writefile{toc}{\contentsline {section}{\numberline {2}Background and Tools}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Basic Notions and Notation}{7}}
\newlabel{corollary wellfounded}{{2.1}{7}}
\citation{klopdiss}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}A Generalized Theorem as the Main Tool}{8}}
\newlabel{theorem a la klop}{{2.2}{8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Terms, Formulas, Substitutions, Contexts}{9}}
\newlabel{corollary substitution B}{{2.4}{10}}
\newlabel{corollary substitution A}{{2.5}{10}}
\@writefile{toc}{\contentsline {section}{\numberline {3}The Concrete Rewrite Relation}{11}}
\newlabel{corollary innermost is always}{{3.1}{11}}
\newlabel{corollary para refltrans}{{3.2}{11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Local Confluence}{11}}
\newlabel{lemma overlapping locally confluent}{{3.3}{11}}
\newlabel{corollary epsilon is confluent}{{3.4}{13}}
\newlabel{corollary epsilon is confluent vacuous}{{3.5}{13}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Well-Founded\discretionary {-}{}{}ness}{13}}
\newlabel{corollary 0 wellfounded}{{3.6}{13}}
\newlabel{theorem epsilon terminates}{{3.7}{13}}
\citation{newman}
\citation{wirthcardinal}
\citation{SR--2011--01}
\citation{wirth-jal}
\citation{grundlagen-first-edition-volume-two}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Confluence}{14}}
\newlabel{theorem epsilon confluent}{{3.8}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}On the Length of Derivations}{14}}
\newlabel{theorem length of derivations}{{3.9}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Conclusion}{14}}
\bibdata{herbrandbib}
\bibcite{ackermann-1925}{\citeauthoryear {Ackermann\ackermannindex }{1925}}
\bibcite{anon-1899}{\citeauthoryear {Anon}{1899}}
\bibcite{workshopontermination2004}{\citeauthoryear {Codish \bgroup \&\ \egroup Middeldorp}{2004}}
\bibcite{writing-mathematics}{\citeauthoryear {Gillman}{1987}}
\bibcite{heijenoort-source-book}{\citeauthoryear {Heijenoort{\index {Heijenoort, Jean van (1912--1986)}}}{1971}}
\bibcite{grundlagen-der-geometrie}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1899}}
\citation{anon-1899}
\citation{hilbert-2004}
\citation{grundlagen-der-geometrie-siebte}
\citation{grundlagen-der-geometrie-neunte}
\citation{grundlagen-der-geometrie-neunte}
\citation{grundlagen-der-geometrie-zehnte}
\citation{grundlagen-der-geometrie-elfte}
\citation{principes-fondamentaux-de-la-geometrie}
\citation{foundations-of-geometry}
\citation{foundations-of-geometry-second}
\bibcite{hilbert-zahlbegriff}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1900a}}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-fuenfte}
\citation{grundlagen-der-geometrie-sechste}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{principes-fondamentaux-de-la-geometrie}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1900b}}
\citation{grundlagen-der-geometrie}
\bibcite{foundations-of-geometry}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1902}}
\citation{grundlagen-der-geometrie}
\bibcite{grundlagen-der-geometrie-zweite}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1903}}
\citation{grundlagen-der-geometrie}
\bibcite{hilbert-grundlagen-logik}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1905}}
\citation{dritter-mathematiker}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-fuenfte}
\citation{grundlagen-der-geometrie-sechste}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{grundlagen-der-geometrie-dritte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1909}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-zweite}
\citation{hilbert-zahlbegriff}
\citation{hilbert-grundlagen-logik}
\bibcite{grundlagen-der-geometrie-vierte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1913}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-dritte}
\bibcite{grundlagen-der-geometrie-fuenfte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1922}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-vierte}
\bibcite{grundlagen-der-geometrie-sechste}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1923}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-fuenfte}
\bibcite{unendliche}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1926}}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{grundlagenvortrag}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1928}}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{probleme-grundlegung}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1930a}}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{grundlagen-der-geometrie-siebte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1930b}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-sechste}
\citation{unendliche}
\citation{grundlagenvortrag}
\citation{probleme-grundlegung}
\bibcite{grundlagen-der-geometrie-achte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1956}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{grundlagen-der-geometrie-neunte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1962}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-achte}
\bibcite{grundlagen-der-geometrie-zehnte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1968}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-neunte}
\bibcite{foundations-of-geometry-second}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1971}}
\citation{foundations-of-geometry}
\citation{grundlagen-der-geometrie-zehnte}
\bibcite{grundlagen-der-geometrie-elfte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1972}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-zehnte}
\bibcite{hilbert-2004}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{2004}}
\bibcite{grundlagen-first-edition-volume-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1934}}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-german-english-edition-volume-one-one}
\citation{grundlagen-german-english-edition-volume-one-one}
\citation{grundlagen-german-english-edition-volume-one-two}
\bibcite{grundlagen-first-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1939}}
\citation{grundlagen-second-edition-volume-two}
\bibcite{grundlagen-second-edition-volume-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1968}}
\citation{grundlagen-first-edition-volume-one}
\citation{grundlagen-german-english-edition-volume-one-one}
\citation{grundlagen-german-english-edition-volume-one-one}
\citation{grundlagen-german-english-edition-volume-one-two}
\bibcite{grundlagen-second-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1970}}
\citation{grundlagen-first-edition-volume-two}
\bibcite{grundlagen-german-english-edition-volume-one-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{2016a}}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-first-edition-volume-one}
\bibcite{grundlagen-german-english-edition-volume-one-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{2016b}}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-first-edition-volume-one}
\bibcite{JouannaudOkadaLICS1991}{\citeauthoryear {Jouannaud \bgroup \&\ \egroup Okada}{1991}}
\citation{lics6}
\bibcite{raamsdonktermination}{\citeauthoryear {Ketema \bgroup \&\ \egroup Raamsdonk}{2004}}
\citation{workshopontermination2004}
\bibcite{klopdiss}{\citeauthoryear {Klop}{1980}}
\bibcite{klopCRS1993}{\citeauthoryear {Klop \bgroup \&al.\egroup }{1993}}
\bibcite{dritter-mathematiker}{\citeauthoryear {Krazer}{1905}}
\bibcite{lics6}{\citeauthoryear {LICS}{1991}}
\bibcite{twelvethRTAone}{\citeauthoryear {Middeldorp}{2001}}
\bibcite{Moore_Wirth_Automation_of_Mathematical_Induction_2013}{\citeauthoryear {Moore{\mooreindex } \bgroup \&\ \egroup Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2014}}
\bibcite{tenthRTAninetynine}{\citeauthoryear {Narendran \bgroup \&\ \egroup Rusinowitch}{1999}}
\bibcite{newman}{\citeauthoryear {Newman}{1942}}
\bibcite{nipkowLICS1991}{\citeauthoryear {Nipkow}{1991}}
\citation{lics6}
\bibcite{Raamsdonk99}{\citeauthoryear {Raamsdonk}{1999}}
\citation{tenthRTAninetynine}
\bibcite{Raamsdonk01}{\citeauthoryear {Raamsdonk}{2001}}
\citation{twelvethRTAone}
\bibcite{twentyfourthRTAthirteen}{\citeauthoryear {Raamsdonk}{2013}}
\bibcite{tait-termination-simply-typed}{\citeauthoryear {Tai{\index {Tait, William W. (*1929)}}t}{1967}}
\bibcite{middeldorp_goodstein}{\citeauthoryear {Winkler \bgroup \&al.\egroup }{2013}}
\citation{twentyfourthRTAthirteen}
\bibcite{wirthcardinal}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2004}}
\bibcite{wirth-jal}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2008}}
\bibcite{wirth-jsc}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2009}}
\bibcite{SR--2011--01}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2015}}