author nipkow Thu Sep 14 17:46:00 2000 +0200 (2000-09-14) changeset 9958 67f2920862c7 child 9993 c0f7fb6e538e permissions -rw-r--r--
*** empty log message ***
     1 \chapter{Advanced Simplification, Recursion, and Induction}

     2 \markboth{}{CHAPTER 4: ADVANCED}

     3

     4 Although we have already learned a lot about simplification, recursion and

     5 induction, there are some advanced proof techniques that we have not covered

     6 yet and which are worth knowing about if you intend to beome a serious

     7 (human) theorem prover. The three sections of this chapter are almost

     8 independent of each other and can be read in any order. Only the notion of

     9 \emph{congruence rules}, introduced in the section on simplification, is

    10 required for parts of the section on recursion.

    11

    12 \input{document/simp.tex}

    13

    14 \section{Advanced forms of recursion}

    15 \label{sec:advanced-recdef}

    16 \index{*recdef|(}

    17 \input{../Recdef/document/Nested0.tex}

    18 \input{../Recdef/document/Nested1.tex}

    19 \input{../Recdef/document/Nested2.tex}

    20 \index{*recdef|)}

    21

    22 \section{Advanced induction techniques}

    23 \label{sec:advanced-ind}

    24 \index{induction|(}

    25 \input{../Misc/document/AdvancedInd.tex}

    26 \index{induction|)}