The solution to this problem is written in Isabelle2013-2. The solution is a collection of primitive recursive functions. The Isabelle theory files are here: Problem2.
There are 3 files:
- PartitionAlgorithm.thy – the implementation of the algorithm
- PartitionProofs.thy - The definitions of the invariants and all proofs
- PartitionTasks.thy – The proofs for the tasks.