\chapter{Advanced Simplification, Recursion and Induction}
\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}
Although we have already learned a lot about simplification, recursion and
induction, there are some advanced proof techniques that we have not covered
yet and which are worth knowing about if you intend to beome a serious
(human) theorem prover. The three sections of this chapter are almost
independent of each other and can be read in any order. Only the notion of
\emph{congruence rules}, introduced in the section on simplification, is
required for parts of the section on recursion.
\input{Advanced/document/simp.tex}
\section{Advanced forms of recursion}
\index{*recdef|(}
\subsection{Recursion over nested datatypes}
\label{sec:nested-recdef}
\input{Recdef/document/Nested0.tex}
\input{Recdef/document/Nested1.tex}
\input{Recdef/document/Nested2.tex}
\index{*recdef|)}
\subsection{Beyond measure}
\label{sec:wellfounded}
\input{Recdef/document/WFrec.tex}
\section{Advanced induction techniques}
\label{sec:advanced-ind}
\index{induction|(}
\input{Misc/document/AdvancedInd.tex}
\index{induction|)}