\begin{thebibliography}{9}

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1925}]{acke%
rmann-1925}
Wilhelm Ackermann\protect\ackermannindex.
\newblock {Begr\ue ndung des \glqq tertium non datur\grqq\ mittel\es\ der
  \hilbert\-schen Theorie der Widerspruch\esi freiheit}.
\newblock {\em {\MathematischeAnnalen}}, 93:1--36, 1925.
\newblock Received \Mar\,30, 1924. Inauguraldissertation, \Goettingen\,1924.

\bibitem[\protect\citeauthoryear{Codish \bgroup\&\ \egroup
  Middeldorp}{2004}]{workshopontermination2004}
Michael Codish and Aart Middeldorp.
\newblock {\nth 7 \Int\ Workshop on Termination (WST), 2004}.
\newblock Technical Report AIB--2004--07, RWTH Aachen, \Dept\ of \CS, 2004.
\newblock ISSN 0935--3232.
  \url{http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2004/2004-07.%
ps.gz}.

\bibitem[\protect\citeauthoryear{Gillman}{1987}]{writing-mathematics}
Leonard Gillman.
\newblock {\em Writing Mathematics Well}.
\newblock The Mathematical Association of America, 1987.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1971}]%
{heijenoort-source-book}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {\em From {\frege} to {\namefont G\"odel}: A Source Book in
  Mathematical Logic, 1879--1931}.
\newblock {\harvardunipress}, 1971.
\newblock {\nth 2\,\rev\ \edn\ (\nth 1\,\edn\,1967)}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1934}]{grundlagen-first-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex\ --- Erster Band}}.
\newblock Number~XL in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}, 1934.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-one}). English translation is
  \makeaciteoftwo{grundlagen-german-english-edition-volume-one-one}{grundlagen%
-german-english-edition-volume-one-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1939}]{grundlagen-first-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex\ --- Zweiter Band}}.
\newblock Number~L in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}, 1939.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-two}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1968}]{grundlagen-second-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex~I}}.
\newblock Number~40 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}, 1968.
\newblock \nth 2\,\rev\,\edn\,of \cite{grundlagen-first-edition-volume-one}.
  English translation is
  \makeaciteoftwo{grundlagen-german-english-edition-volume-one-one}{grundlagen%
-german-english-edition-volume-one-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1970}]{grundlagen-second-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex~II}}.
\newblock Number~50 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}, 1970.
\newblock \nth 2\,\rev\,\edn\,of \cite{grundlagen-first-edition-volume-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{2016a}]{grundlagen-german-english-edition-v%
olume-one-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,A: \whatisinVolIPartA}}.
\newblock {\springerverlag}, 2016.
\newblock First English translation and bilingual facsimile \edn\ of the \nth 2
  German \edn\ \cite{grundlagen-second-edition-volume-one}, \incl\ the
  annotation and translation of all differences of the \nth 1 German \edn\
  \cite{grundlagen-first-edition-volume-one}. \ \Ed\ by \wirthname,
  \siekmannname, \michaelgabbayname, \gabbayname. \ Advisory Board: \siegname\
  (chair), \anellisname, \awodeyname, \baazname, \buchholzname, \buldtname,
  \kahlename, \mancosuname, \parsonsname, \peckhausname, \taitname, \tappname,
  \zachname. \ Translated and commented by \wirthname\ \etalabbrev\ Thoroughly
  \rev\ \nth 3\,\edn\ (\nth 1\,\edn\ \collegepublications, 2011; \nth 2\,\edn\
  \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{2016b}]{grundlagen-german-english-edition-v%
olume-one-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex}.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,B: \whatisinVolIPartB}}.
\newblock {\springerverlag}, 2016.
\newblock First English translation and bilingual facsimile \edn\ of the \nth 2
  German \edn\ \cite{grundlagen-second-edition-volume-one}, \incl\ the
  annotation and translation of all deleted texts of the \nth 1 German \edn\
  \cite{grundlagen-first-edition-volume-one}. \ \Ed\ by \wirthname,
  \siekmannname, \michaelgabbayname, \gabbayname. \ Advisory Board: \siegname\
  (chair), \anellisname, \awodeyname, \baazname, \buchholzname, \buldtname,
  \kahlename, \mancosuname, \parsonsname, \peckhausname, \taitname, \tappname,
  \zachname. \ Translated and commented by \wirthname\ \etalabbrev\ Thoroughly
  \rev\ \nth 3\,\edn\ (\nth 1\,\edn\ \collegepublications, 2012; \nth 2\,\edn\
  \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1926}]{unend%
liche}
David Hilbe{\protectedhilbertindex}rt.
\newblock {\Ue ber das Unendliche --- Vortrag, gehalten am 4.\,Juni\,1925
  gelegentlich einer zur Ehrung de\es\ Andenken\es\ an \weierstrass\ von der
  West\-f\ae lischen \Math\ \Ges\ veranstalteten Mathematiker-Zusammenkunft in
  M\ue nster i. W.}
\newblock {\em {\MathematischeAnnalen}}, 95:161--190, 1926.
\newblock Received \Jun\,24, 1925. \ {E}nglish translation {\em On the
  infinite} by \bauermengelbergname\ with an introduction by \heijenoortname\
  in \cite[\PP{367}{392}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1928}]{grund%
lagenvortrag}
David Hilbe{\protectedhilbertindex}rt.
\newblock {Die \grundlagendermathematiknoindex\ --- Vortrag, gehalten auf
  Einladung des Mathematischen Seminars im Juli 1927 in \Hamburg}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:65--85, 1928.
\newblock {E}nglish translation {\em The foundations of mathematics}\/ by
  \bauermengelbergname\protect\ and \foellesdalname\ with a short introduction
  by \heijenoortname\ in \cite[\PP{464}{479}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Jouannaud \bgroup\&\ \egroup
  Okada}{1991}]{JouannaudOkadaLICS1991}
Jean-Pierre Jouannaud and Mitsuhiro Okada.
\newblock A computation-model for executable higher-order algebraic
  specification languages.
\newblock 1991.
\newblock In \cite[\PP{350}{361}]{lics6}.

\bibitem[\protect\citeauthoryear{Ketema \bgroup\&\ \egroup
  Raamsdonk}{2004}]{raamsdonktermination}
Jeroen Ketema and Femke~van Raamsdonk.
\newblock Erasure and termination in higher-order rewriting.
\newblock 2004.
\newblock In \cite[\PP{30}{33}]{workshopontermination2004}. Also available at
  \url{www.prove-and-die.org/publ/wst04.pdf}.

\bibitem[\protect\citeauthoryear{Klop \bgroup\&al.\egroup }{1993}]{klopCRS1993}
Jan~Willem Klop, Vincent~van Oostrom, and Femke~van Raamsdonk.
\newblock Combinatory reduction systems: introduction and survey.
\newblock {\em \tcsname}, 121:279--308, 1993.

\bibitem[\protect\citeauthoryear{Klop}{1980}]{klopdiss}
Jan~Willem Klop.
\newblock Combinatory reduction systems.
\newblock Mathematical centre tracts 127, {Mathematisch Centrum (since 1983:
  Centrum Wiskunde \& Informatica), \Amsterdam}, 1980.
\newblock \PhDthesis, Utrecht \Univ.,
  \url{http://libgen.io/get.php?md5=a80df1dda74dffd97700bda2277e8bc4}.

\bibitem[\protect\citeauthoryear{LICS}{1991}]{lics6}
{\em {\Proc\ \nth 6 \LICSname, \Amsterdam, 1991}}. \ieeepress, 1991.
\newblock \licsarchive\url{1991}.

\bibitem[\protect\citeauthoryear{Middeldorp}{2001}]{twelvethRTAone}
Aart Middeldorp, editor.
\newblock {\em {\thetwelvethRTAone}}, number 2051 in Lecture Notes in Computer
  Science. {\springerverlag}, 2001.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex} \bgroup\&\ \egroup
  Wirth{\protectedwirthindex}}{2014}]{Moore_Wirth_Automation_of_Mathematical_I%
nduction_2013}
J~Strother Moore{\protect\mooreindex} and Claus-Peter
  Wirth{\protectedwirthindex}.
\newblock {\em {Automation of Mathematical Induction as part of the History of
  Logic}}.
\newblock {SEKI-Report SR--2013--02 (ISSN 1437--4447)}. {SEKI Publications},
  2014.
\newblock \Rev\,\edn\ \Jul\,2014 (\nth 1\,\edn\,2013), \PPcount{ii+107},
  \url{http://arxiv.org/abs/1309.6226}.

\bibitem[\protect\citeauthoryear{Narendran \bgroup\&\ \egroup
  Rusinowitch}{1999}]{tenthRTAninetynine}
Paliath Narendran and Micha{\"e}l Rusinowitch, editors.
\newblock {\em {\thetenthRTAninetynine}}, number 1631 in Lecture Notes in
  Computer Science. {\springerverlag}, 1999.

\bibitem[\protect\citeauthoryear{Newman}{1942}]{newman}
Max H.~A. Newman.
\newblock On theories with a combinatorial definition of equivalence.
\newblock {\em \annalsofmathematicsname}, 43:223--242, 1942.

\bibitem[\protect\citeauthoryear{Nipkow}{1991}]{nipkowLICS1991}
Tobias Nipkow.
\newblock Higher-order critical pairs.
\newblock 1991.
\newblock In \cite[\PP{342}{349}]{lics6}.

\bibitem[\protect\citeauthoryear{Raamsdonk}{1999}]{Raamsdonk99}
Femke~van Raamsdonk.
\newblock Higher-order rewriting.
\newblock 1999.
\newblock In \cite[\PP{221}{239}]{tenthRTAninetynine}.

\bibitem[\protect\citeauthoryear{Raamsdonk}{2001}]{Raamsdonk01}
Femke~van Raamsdonk.
\newblock On termination of higher-order rewriting.
\newblock 2001.
\newblock In \cite[\PP{261}{275}]{twelvethRTAone}.

\bibitem[\protect\citeauthoryear{Raamsdonk}{2013}]{twentyfourthRTAthirteen}
Femke~van Raamsdonk, editor.
\newblock {\em {\thetwentyfourthRTAthirteen}}, number~24 in Leibniz \Int\
  \Proc\ in Informatics. Dagstuhl (Germany), 2013.

\bibitem[\protect\citeauthoryear{Tai{\protectedtaitindex}t}{1967}]{tait-termin%
ation-simply-typed}
William~W. Tai{\protectedtaitindex}t.
\newblock Intensional interpretations of functionals of finite type {I}.
\newblock {\em \jslname}, 32:198--212, 1967.

\bibitem[\protect\citeauthoryear{Winkler \bgroup\&al.\egroup
  }{2013}]{middeldorp_goodstein}
Sarah Winkler, Harald Zankl, and Aart Middeldorp.
\newblock {Beyond \peano\ Arithmetic} --- automatically proving termination of
  the {\goodstein} sequence.
\newblock 2013.
\newblock In \cite[\PP{335}{351}]{twentyfourthRTAthirteen}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2004}]{wirthcard%
inal}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\DescenteInfinie\ + Deduction}.
\newblock {\em {\ljigplname}}, 12:1--96, 2004.
\newblock \www\url{/p/d}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2008}]{wirth-jal}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic}, 6:287--317, 2008.
\newblock \url{http://dx.doi.org/10.1016/j.jal.2007.07.009}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2009}]{wirth-jsc}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em {\jscname}}, 44:69--98, 2009.
\newblock \url{http://dx.doi.org/10.1016/j.jsc.2008.05.005}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2015}]{SR--2011--01}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em {A Simplified and Improved Free-Variable Framework for
  \hilbert's epsilon as an Operator of Indefinite Committed Choice}}.
\newblock {SEKI Report SR--2011--01 (ISSN 1437--4447)}. {SEKI Publications},
  2015.
\newblock \Rev\,\edn\ \Jun\,2015 (\nth 1\,\edn\,2011), \PPcount{ii+82},
  {\url{http://arxiv.org/abs/1104.2444}}.

\end{thebibliography}