\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1925}]{acke%
rmann-1925}
Wilhelm Ackermann\protect\ackermannindex, 1925.
\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.
\newblock Received \Mar\,30, 1924. Inauguraldissertation, 1924, \Goettingen.

\bibitem[\protect\citeauthoryear{Anon}{1899}]{anon-1899}
Anon, editor, 1899.
\newblock {\em {Festschrift zur Feier der Enth\ue llung des\/
  \gauss-\weber-Denkmals in \Goettingen, herau\esi gegeben von dem
  Fest-Comitee.}}
\newblock Verlag von B. G. Teubner, \Leipzig.

\bibitem[\protect\citeauthoryear{Codish \bgroup\&\ \egroup
  Middeldorp}{2004}]{workshopontermination2004}
Michael Codish and Aart Middeldorp, 2004.
\newblock {\nth 7 \Int\ Workshop on Termination (WST), 2004}.
\newblock Technical Report AIB--2004--07, RWTH Aachen, \Dept\ of \CS.
\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, 1987.
\newblock {\em Writing Mathematics Well}.
\newblock The Mathematical Association of America.

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

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1899}]{grund%
lagen-der-geometrie}
David Hilbe{\protectedhilbertindex}rt, 1899.
\newblock {\grundlagendergeometrienoindex}.
\newblock In \cite[\PP{1}{92}]{anon-1899}. \nth 1\,\edn\ without \appendixes.
  Reprinted in \cite[\PP{436}{525}]{hilbert-2004}\bibcrit{Last edition of
  ``\grundlagendergeometrienoindex'' by \hilbert\ is
  \cite{grundlagen-der-geometrie-siebte}, which is also most complete regarding
  the appendixes. Last three editions by\/ \bernaysname\ are
  \makeaciteofthree{grundlagen-der-geometrie-neunte}{grundlagen-der-geometrie-%
zehnte}{grundlagen-der-geometrie-elfte}, which are also most complete regarding
  supplements and figures. Its first appearance as a separate book was the
  French translation \cite{principes-fondamentaux-de-la-geometrie}. Two
  substantially different {English} translations are
  \cite{foundations-of-geometry} and \cite{foundations-of-geometry-second}}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1900a}]{hilb%
ert-zahlbegriff}
David Hilbe{\protectedhilbertindex}rt, 1900a.
\newblock {\Ue ber den Zahlbegriff}.
\newblock {\em \dmvjahresberichtname}, 8:180--184.
\newblock Received \Dec\,1899. Reprinted as {Appendix\,VI} of
  \makeaciteoffive{grundlagen-der-geometrie-dritte}{grundlagen-der-geometrie-v%
ierte}{grundlagen-der-geometrie-fuenfte}{grundlagen-der-geometrie-sechste}{gru%
ndlagen-der-geometrie-siebte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1900b}]{prin%
cipes-fondamentaux-de-la-geometrie}
David Hilbe{\protectedhilbertindex}rt, 1900b.
\newblock Les principes fondamentaux de la g{\'e}om{\'e}trie.
\newblock {\em Annales Scientifiques de l'\EcoleNormaleSuperieure},
  S\'erie\,3,\,17:103--209.
\newblock {French} translation by {\namefont L\'eonce Laugel} of special
  version of \cite{grundlagen-der-geometrie}, revised and authorized by
  \hilbert. Also in published as a separate book by the same publisher
  (\gauthiervillars).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1902}]{found%
ations-of-geometry}
David Hilbe{\protectedhilbertindex}rt, 1902.
\newblock {\em The Foundations of Geometry}.
\newblock Open Court, \Chicago.
\newblock {English} translation by {\namefont E. J. Townsend} of special
  version of \cite{grundlagen-der-geometrie}, revised and authorized by
  \hilbert, \url{http://www.gutenberg.org/etext/17384}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1903}]{grund%
lagen-der-geometrie-zweite}
David Hilbe{\protectedhilbertindex}rt, 1903.
\newblock {\em {\grundlagendergeometrienoindex. --- Zweite, durch Zus\ae tze
  vermehrte und mit f\ue nf Anh\ae ngen versehene Au\fli age. Mit zahlreichen
  in den Text gedruckten Figuren}}.
\newblock Druck und Verlag von B. G. Teubner, \Leipzig.
\newblock {\nth 2}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\ and \extd\ with five \appendixes, newly added figures, and an index of
  notion names.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1905}]{hilbe%
rt-grundlagen-logik}
David Hilbe{\protectedhilbertindex}rt, 1905.
\newblock {\Ue ber die Grundlagen der Logik und der Arithmetik}.
\newblock In \cite[\PP{174}{185}]{dritter-mathematiker}. \ Reprinted as
  {Appendix\,VII} of
  \makeaciteoffive{grundlagen-der-geometrie-dritte}{grundlagen-der-geometrie-v%
ierte}{grundlagen-der-geometrie-fuenfte}{grundlagen-der-geometrie-sechste}{gru%
ndlagen-der-geometrie-siebte}. \ {English} translation {\em On the foundations
  of logic and arithmetic} by {\namefont Beverly Woodward} with an introduction
  by \heijenoortname\ in \cite[\PP{129}{138}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1909}]{grund%
lagen-der-geometrie-dritte}
David Hilbe{\protectedhilbertindex}rt, 1909.
\newblock {\em {\grundlagendergeometrienoindex. --- Dritte, durch Zus\ae tze
  und Literaturhinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahlreichen in den Text gedruckten Figuren.}}
\newblock Number VII in Wissenschaft und Hypothese. Druck und Verlag von B. G.
  Teubner, \Leipzig, \Berlin.
\newblock {\nth 3}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-zweite}, \extd\ with a
  bibliography and two additional \appendixes\ (now seven in total)
  (Appendix\,VI: \cite{hilbert-zahlbegriff}) (Appendix\,VII:
  \cite{hilbert-grundlagen-logik}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1913}]{grund%
lagen-der-geometrie-vierte}
David Hilbe{\protectedhilbertindex}rt, 1913.
\newblock {\em {\grundlagendergeometrienoindex. --- Vierte, durch Zus\ae tze
  und Literaturhinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahlreichen in den Text gedruckten Figuren.}}
\newblock Druck und Verlag von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 4}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-dritte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1922}]{grund%
lagen-der-geometrie-fuenfte}
David Hilbe{\protectedhilbertindex}rt, 1922.
\newblock {\em {\grundlagendergeometrienoindex. --- F\ue nfte, durch Zus\ae tze
  und Literatur\-hinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahl\-reichen in den Text gedruckten Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 5}\,\extd\,\edn\,of \cite{grundlagen-der-geometrie}. \ Contrary
  to what the sub-title may suggest, this is an anastatic reprint of
  \cite{grundlagen-der-geometrie-vierte}, extended by a very short preface on
  the changes \wrt\ \cite{grundlagen-der-geometrie-vierte}, and with
  augmentations to Appendix\,II, Appendix\,III, and \litchapref{IV},
  \litsectref{21}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1923}]{grund%
lagen-der-geometrie-sechste}
David Hilbe{\protectedhilbertindex}rt, 1923.
\newblock {\em {\grundlagendergeometrienoindex. --- Sechste unver\ae nderte
  Au\fli age. Anastati\-scher Nachdruck. Mit zahlreichen in den Text gedruckten
  Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 6}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  anastatic reprint of \cite{grundlagen-der-geometrie-fuenfte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1926}]{unend%
liche}
David Hilbe{\protectedhilbertindex}rt, 1926.
\newblock {\Ue ber da\es\ 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.
\newblock Received \Jun\,24, 1925. \ Reprinted as Appendix\,VIII of
  \cite{grundlagen-der-geometrie-siebte}. \ {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, 1928.
\newblock {Die \grundlagendermathematiknoindex\ --- Vortrag, gehalten auf
  Einladung des Mathematischen Seminars im Juli 1927 in \Hamburg}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:65--85.
\newblock Reprinted as Appendix\,IX of \cite{grundlagen-der-geometrie-siebte}.
  \ {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{Hilbe{\protectedhilbertindex}rt}{1930a}]{prob%
leme-grundlegung}
David Hilbe{\protectedhilbertindex}rt, 1930a.
\newblock {Probleme der Grundlegung der Mathematik}.
\newblock {\em {\MathematischeAnnalen}}, 102:1--9.
\newblock {Vortrag gehalten auf dem Internationalen Mathematiker-Kongre\sz\ in
  \Bologna, \Sep\,3, 1928}. \ Received March\,25, 1929. \ Reprinted as
  Appendix\,X of \cite{grundlagen-der-geometrie-siebte}. \ Short version in
  {\em Atti del congresso internationale dei matematici, \Bologna, 3--10
  settembre 1928}, \Vol\,1, \PP{135}{141}, Bologna, 1929.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1930b}]{grun%
dlagen-der-geometrie-siebte}
David Hilbe{\protectedhilbertindex}rt, 1930b.
\newblock {\em {\grundlagendergeometrienoindex. --- Siebente umgearbeitete und
  vermehrte Au\fli age. Mit 100 in den Text gedruckten Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 7}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  thoroughly revised edition of \cite{grundlagen-der-geometrie-sechste}, \extd\
  with three new \appendixes\ (now ten in total) (Appendix\,VIII:
  \cite{unendliche}) (Appendix\,IX: \cite{grundlagenvortrag}) (Appendix\,X:
  \cite{probleme-grundlegung}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1956}]{grund%
lagen-der-geometrie-achte}
David Hilbe{\protectedhilbertindex}rt, 1956.
\newblock {\em {\grundlagendergeometrienoindex. --- Achte Au\fli age, mit
  Revisionen und Erg\ae nzungen von \Dr\ \bernaysname. Mit 124 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth 8}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-siebte}, omitting \appendixes\
  VI--X, \extd\ by \bernaysname, now with 24 additional figures and 3
  additional supplements.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1962}]{grund%
lagen-der-geometrie-neunte}
David Hilbe{\protectedhilbertindex}rt, 1962.
\newblock {\em {\grundlagendergeometrienoindex. --- Neunte Au\fli age,
  revidiert und erg\ae nzt von \Dr\ \bernaysname. Mit 129 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth 9}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-achte}, \extd\ by \bernaysname,
  now with 129\,figures, 5\,\appendixes, and 8\,supplements (I\,1, I\,2, II,
  III, IV\,1, IV\,2, V\,1, V\,2).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1968}]{grund%
lagen-der-geometrie-zehnte}
David Hilbe{\protectedhilbertindex}rt, 1968.
\newblock {\em {\grundlagendergeometrienoindex. --- Zehnte Au\fli age,
  revidiert und erg\ae nzt von \Dr\ \bernaysname. Mit 124 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth{10}}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-neunte} by \bernaysname.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1971}]{found%
ations-of-geometry-second}
David Hilbe{\protectedhilbertindex}rt, 1971.
\newblock {\em The Foundations of Geometry}.
\newblock Open Court, \Chicago\ and La Salle (IL).
\newblock Newly translated and fundamentally different \nth 2\,\edn\,of
  \cite{foundations-of-geometry}, actually an English translation of
  \cite{grundlagen-der-geometrie-zehnte} by {\namefont Leo Unger}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1972}]{grund%
lagen-der-geometrie-elfte}
David Hilbe{\protectedhilbertindex}rt, 1972.
\newblock {\em {\grundlagendergeometrienoindex. --- 11.\,Au\fli age. Mit
  Supplementen von \Dr\ \bernaysname}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth{11}}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-zehnte} by \bernaysname.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{2004}]{hilbe%
rt-2004}
David Hilbe{\protectedhilbertindex}rt, 2004.
\newblock {\em {\hilbertname}'s Lectures on the Foundations of Geometry,
  1891--1902}.
\newblock {\springerverlag}.
\newblock \Ed\ by \hallettname\ and \majername.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1934}]{grundlagen-first-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1934.
\newblock {\em {\grundlagendermathematiknoindex\ --- \mbox{Erster} Band}}.
\newblock Number~XL in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-one}). Reprinted by J.\,W.\,Edwards
  \Publ, Ann Arbor (MI), 1944. 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},
  1939.
\newblock {\em {\grundlagendermathematiknoindex\ --- \mbox{Zweiter} Band}}.
\newblock Number~L in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-two}). Reprinted by J.\,W.\,Edwards
  \Publ, Ann Arbor (MI), 1944.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1968}]{grundlagen-second-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1968.
\newblock {\em {\grundlagendermathematiknoindex~I}}.
\newblock Number~40 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\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},
  1970.
\newblock {\em {\grundlagendermathematiknoindex~II}}.
\newblock Number~50 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 2\,\rev\,\extd\,\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},
  2016a.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,A: \whatisinVolIPartA}}.
\newblock {\springerverlag}.
\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, \peckhausname, \michaelgabbayname, \gabbayname. \ 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},
  2016b.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,B: \whatisinVolIPartB}}.
\newblock {\springerverlag}.
\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, \peckhausname, \michaelgabbayname, \gabbayname. \ 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{Jouannaud \bgroup\&\ \egroup
  Okada}{1991}]{JouannaudOkadaLICS1991}
Jean-Pierre Jouannaud and Mitsuhiro Okada, 1991.
\newblock A computation-model for executable higher-order algebraic
  specification languages.
\newblock In \cite[\PP{350}{361}]{lics6}.

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

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

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

\bibitem[\protect\citeauthoryear{Krazer}{1905}]{dritter-mathematiker}
A.~Krazer, editor, 1905.
\newblock {\em {Verhandlungen des Dritten Internationalen
  Mathematiker-Kongresses, Heidelberg, \Aug\,8--13, 1904}}. Verlag von B. G.
  Teubner, \Leipzig.

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

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

\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}, 2014.
\newblock {\em {Automation of Mathematical Induction as part of the History of
  Logic}}.
\newblock {SEKI-Report SR--2013--02 (ISSN 1437--4447)}. {SEKI Publications}.
\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, 1999.
\newblock {\em {\thetenthRTAninetynine}}, number 1631 in Lecture Notes in
  Computer Science. {\springerverlag}.

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2008}]{wirth-jal}
Claus-Peter Wirth{\protectedwirthindex}, 2008.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic}, 6:287--317.
\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}, 2009.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em {\jscname}}, 44:69--98.
\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}, 2015.
\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}.
\newblock \Rev\,\edn\ \Jun\,2015 (\nth 1\,\edn\,2011), \PPcount{ii+82},
  {\url{http://arxiv.org/abs/1104.2444}}.

\end{thebibliography}
