7 (human) theorem prover. The three sections of this chapter are almost |
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 |
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 |
9 \emph{congruence rules}, introduced in the section on simplification, is |
10 required for parts of the section on recursion. |
10 required for parts of the section on recursion. |
11 |
11 |
12 \input{document/simp.tex} |
12 \input{Advanced/document/simp.tex} |
13 |
13 |
14 \section{Advanced forms of recursion} |
14 \section{Advanced forms of recursion} |
15 \label{sec:advanced-recdef} |
15 \label{sec:advanced-recdef} |
16 \index{*recdef|(} |
16 \index{*recdef|(} |
17 \input{../Recdef/document/Nested0.tex} |
17 \input{Recdef/document/Nested0.tex} |
18 \input{../Recdef/document/Nested1.tex} |
18 \input{Recdef/document/Nested1.tex} |
19 \input{../Recdef/document/Nested2.tex} |
19 \input{Recdef/document/Nested2.tex} |
20 \index{*recdef|)} |
20 \index{*recdef|)} |
21 |
21 |
22 \section{Advanced induction techniques} |
22 \section{Advanced induction techniques} |
23 \label{sec:advanced-ind} |
23 \label{sec:advanced-ind} |
24 \index{induction|(} |
24 \index{induction|(} |
25 \input{../Misc/document/AdvancedInd.tex} |
25 \input{Misc/document/AdvancedInd.tex} |
26 \index{induction|)} |
26 \index{induction|)} |