"Unusual" Induction Scheme
--------------------------

001a
001b
001c
002
014
015

Destructor Style Induction
--------------------------

010
013

Lemmata
-------

001a
001b
001c
002
004a
004b
005a
005b
008a
008b
010
012
014
015
016

Higher Order
------------

001b
001c
005a
005b
008b
014
015
018

Problems for Rippling
---------------------

001a
001b
001c
009
011
012
015

Case Analysis
-------------

003
011
012

Equality Theorem
----------------

001a
001b
001c
002
004a
004b
005a
005b
006
008a
008b
009
013
014
015

Generalisation
--------------

004a
011
012
016

Mutual Recursion
----------------

006
007


The Problems
------------

001 - Arithmetic Geometric Mean
002 - Length of the joined list of two lists of even length is even
003 - A member of a list is a member of that list joined to another
004 - Rotate Length
005 - Binomial Theorems
006 - Two definition of Even are equivalent
007 - All numbers are odd or even
008 - Chinese Remainder Theorem
009 - "Pete's Nasty Theorem"
010 - Quicksort
011 - Safety Lemma for Removing the head of an abstract list
012 - Safety Lemma for Prefix Operation
013 - Divide and Conquer
014 - Harald's Problem
015 - Paulson's Problem
016 - The Whiskey Problem
017 - Dixon's Problem