\chapter{Advanced Simplification, Recursion, and Induction}
\markboth{}{CHAPTER 4: ADVANCED}
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}
\label{sec:advanced-recdef}
\index{*recdef|(}
\input{Recdef/document/Nested0.tex}
\input{Recdef/document/Nested1.tex}
\input{Recdef/document/Nested2.tex}
\index{*recdef|)}
\section{Advanced induction techniques}
\label{sec:advanced-ind}
\index{induction|(}
\input{Misc/document/AdvancedInd.tex}
\index{induction|)}