\relax 
\ifx\hyper@anchor\@undefined
\global \let \oldcontentsline\contentsline
\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global \let \oldnewlabel\newlabel
\gdef \newlabel#1#2{\newlabelxx{#1}#2}
\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\let \contentsline\oldcontentsline
\let \newlabel\oldnewlabel}
\else
\global \let \hyper@last\relax 
\fi

\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}{1}{section.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}The Explicit Historical Source of the Problem}{1}{subsection.1.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Subject Matter}{3}{subsection.1.2}}
\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}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}A Lacuna in Hilbert--Bernays?}{4}{subsection.1.3}}
\newlabel{section A Lacuna in}{{1.3}{4}{A Lacuna in Hilbert--Bernays?\relax }{subsection.1.3}{}}
\citation{grundlagen-first-edition-volume-two}
\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}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Alternative Proofs by Applying Theories of First- or Higher-Order Rewriting?}{5}{subsection.1.4}}
\citation{klopCRS1993}
\citation{klopdiss}
\citation{klopCRS1993}
\citation{klopdiss}
\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}
\@writefile{toc}{\contentsline {section}{\numberline {2}Background and Tools}{7}{section.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Basic Notions and Notation}{7}{subsection.2.1}}
\citation{klopdiss}
\citation{Moore_Wirth_Automation_of_Mathematical_Induction_2013}
\newlabel{corollary wellfounded}{{2.1}{8}{Basic Notions and Notation\relax }{theorem.2.1}{}}
\citation{klopdiss}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}A Generalized Theorem as the Main Tool}{9}{subsection.2.2}}
\newlabel{theorem a la klop}{{2.2}{9}{A Generalized Theorem as the Main Tool\relax }{theorem.2.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Terms, Formulas, Substitutions, Contexts}{11}{subsection.2.3}}
\newlabel{corollary substitution B}{{2.4}{12}{Terms, Formulas, Substitutions, Contexts\relax }{theorem.2.4}{}}
\newlabel{corollary substitution A}{{2.5}{12}{Terms, Formulas, Substitutions, Contexts\relax }{theorem.2.5}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}The Concrete Rewrite Relation}{13}{section.3}}
\newlabel{corollary innermost is always}{{3.1}{13}{The Concrete Rewrite Relation\relax }{theorem.3.1}{}}
\newlabel{corollary para refltrans}{{3.2}{13}{The Concrete Rewrite Relation\relax }{theorem.3.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Local Confluence}{13}{subsection.3.1}}
\newlabel{lemma overlapping locally confluent}{{3.3}{14}{Local Confluence\relax }{theorem.3.3}{}}
\newlabel{corollary epsilon is confluent}{{3.4}{15}{Local Confluence\relax }{theorem.3.4}{}}
\newlabel{corollary epsilon is confluent vacuous}{{3.5}{15}{Local Confluence\relax }{theorem.3.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Well-Founded\discretionary {-}{}{}ness}{15}{subsection.3.2}}
\newlabel{corollary 0 wellfounded}{{3.6}{15}{\WellFoundedness \relax }{theorem.3.6}{}}
\citation{newman}
\citation{wirthcardinal}
\newlabel{theorem epsilon terminates}{{3.7}{16}{\WellFoundedness \relax }{theorem.3.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Confluence}{16}{subsection.3.3}}
\newlabel{theorem epsilon confluent}{{3.8}{16}{Confluence\relax }{theorem.3.8}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}On the Length of Derivations}{16}{subsection.3.4}}
\citation{SR--2011--01}
\citation{wirth-jal}
\citation{grundlagen-first-edition-volume-two}
\newlabel{theorem length of derivations}{{3.9}{17}{On the Length of Derivations\relax }{theorem.3.9}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Conclusion}{17}{section.4}}
\bibcite{ackermann-1925}{\citeauthoryear {Ackermann\ackermannindex }{1925}}
\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-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{unendliche}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1926}}
\citation{heijenoort-source-book}
\bibcite{grundlagenvortrag}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1928}}
\citation{heijenoort-source-book}
\bibcite{JouannaudOkadaLICS1991}{\citeauthoryear {Jouannaud \bgroup \&\ \egroup Okada}{1991}}
\citation{lics6}
\bibcite{raamsdonktermination}{\citeauthoryear {Ketema \bgroup \&\ \egroup Raamsdonk}{2004}}
\citation{workshopontermination2004}
\bibcite{klopCRS1993}{\citeauthoryear {Klop \bgroup \&al.\egroup }{1993}}
\bibcite{klopdiss}{\citeauthoryear {Klop}{1980}}
\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}}