\BOOKMARK [1][-]{section.1}{Introduction}{}
\BOOKMARK [2][-]{subsection.1.1}{The Explicit Historical Source of the Problem}{section.1}
\BOOKMARK [2][-]{subsection.1.2}{Subject Matter}{section.1}
\BOOKMARK [2][-]{subsection.1.3}{A Lacuna in Hilbert--Bernays?}{section.1}
\BOOKMARK [2][-]{subsection.1.4}{Alternative Proofs by Applying Theories of First- or Higher-Order Rewriting?}{section.1}
\BOOKMARK [1][-]{section.2}{Background and Tools}{}
\BOOKMARK [2][-]{subsection.2.1}{Basic Notions and Notation}{section.2}
\BOOKMARK [2][-]{subsection.2.2}{A Generalized Theorem as the Main Tool}{section.2}
\BOOKMARK [2][-]{subsection.2.3}{Terms, Formulas, Substitutions, Contexts}{section.2}
\BOOKMARK [1][-]{section.3}{The Concrete Rewrite Relation}{}
\BOOKMARK [2][-]{subsection.3.1}{Local Confluence}{section.3}
\BOOKMARK [2][-]{subsection.3.2}{Well-Foundedness}{section.3}
\BOOKMARK [2][-]{subsection.3.3}{Confluence}{section.3}
\BOOKMARK [2][-]{subsection.3.4}{On the Length of Derivations}{section.3}
\BOOKMARK [1][-]{section.4}{Conclusion}{}