7th TPP (2011) in AIST (Tsukuba) - TPPmark

Problem: 

There are N children sitting in a circle, where each child has an even
number of candies. The following step is repeated indefinitely:

  every child passes half of their candies to the child on their left;
  any child who ends up with an odd number of candies is given another
  candy by the teacher.

Then, prove that eventually every child will hold the same number of
candies.

Proof outline: 

Let m(i,k) be the number of candies held by the i'th
child (i in {1,...,N}) after k steps. At first, prove the following
lemmas:

 (1) max(k+1) <= max(k),
 (2) min(k) <= min(k+1),
 (3) if min(k) < m(i,k) then min(k) < m(i,k+1),
 (4) if m(i,k) < m(right(i),k) then m(i,k) < m(i,k+1),

where

    max(k) = max{m(i,k) | i in {1,...,N}},
    min(k) = min{m(i,k) | i in {1,...,N}},
  right(i) = (if (i < N) then (i+1) else 1).

Then, prove the following lemma:

 (5) if (min(k) < m(i,k)) for some i,
     then num(min(k),k+1) < num(min(k),k),

where

  num(m,k) is the number of children holding m candies after k steps.

Finally, it can be proven that all the children eventually hold the
same number of candies.

Reference:

  1. Bohman, T., Pikhurko, O., Frieze, A., Sleator, D.:
    The Puzzle TOAD, Puzzle 6: Uniform Candy Distribution.
    Carnegie Mellon, School of Computer Science. Solution. Last access: 2011/10/13.

Solutions using theorem provers: