104

1 
\contentsline {section}{\numberline {1}Introduction}{1}

294

2 
\contentsline {section}{\numberline {2}Fixedpoint operators}{1}


3 
\contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2}

104

4 
\contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2}


5 
\contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3}

294

6 
\contentsline {subsection}{\numberline {3.3}Mutual recursion}{3}

104

7 
\contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4}


8 
\contentsline {subsection}{\numberline {3.5}The elimination rule}{4}

294

9 
\contentsline {section}{\numberline {4}Induction and coinduction rules}{4}


10 
\contentsline {subsection}{\numberline {4.1}The basic induction rule}{4}

104

11 
\contentsline {subsection}{\numberline {4.2}Mutual induction}{5}

294

12 
\contentsline {subsection}{\numberline {4.3}Coinduction}{5}


13 
\contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6}


14 
\contentsline {subsection}{\numberline {5.1}The finite set operator}{6}


15 
\contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{6}


16 
\contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7}


17 
\contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8}


18 
\contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9}


19 
\contentsline {section}{\numberline {6}Datatypes and codatatypes}{11}


20 
\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11}


21 
\contentsline {subsection}{\numberline {6.2}The case analysis operator}{11}


22 
\contentsline {section}{\numberline {7}Conclusions and future work}{12}
