The Coffee Can Problem

Summary
A simple problem involving invariants and termination condition of an iterative process is solved.  A simple property of this iterative process is shown.

This problem appears David Gries's The Science of Programming:
You are given a coffee can that contains beans painted either black or white. Next to the can is a large pile of black beans. You perform the following algorithm:
Let \(N\) be the number of beans in the can at the current instant of time.

1. If \(N=1\), then stop.
2. Randomly draw two beans from the can. Call them \(B_0\) and \(B_1\).
3. If color(\(B_0\)) \(\neq\) color(\(B_1\)), then return white bean to the can and throw away the black bean.
4. If color(\(B_0\)) \(=\) color(\(B_1\)), then throw away both beans and place a black bean from the pile into the can.
5. Go to step 1.

Does the process terminate? If the process does terminate, then what can be said about the remaining bean in the can in terms of the number of black and white beans which were in the can to start with?
Proving that this terminates is easy. Let \(N_b\) be the number of BLACK beans in the can at the current instant of time and let \(N_w\) be the number of WHITE beans in the can at the current instant of time. Also, let \(N'\) be the number of beans in the can after either steps 3 or 4. The following is then true:

1. color(\(B_0\)) \(\neq\) color(\(B_1\)) \(\Rightarrow\)
        \(N'= (N_b - 1) + N_w = N - 1\)
   
2. color(\(B_0\)) \(=\) color(\(B_1\)) \(=\) WHITE \(\Rightarrow\)
        \(N' = (N_b + 1) + (N_w - 2) = N - 1\)
   
3. color(\(B_0\)) \(=\) color(\(B_1\)) \(=\) BLACK \(\Rightarrow\)
        \(N' = (N_b - 1) + N_w = N - 1\)
   

The total number of beans in the can is reduced by one for every iteration of the algorithm and therefore the process terminates when the condition in step 1 is satisfied. (Most people can just work this out in their heads)
"Saying something" about the last remaining bean in terms of the initial number of black and white beans is more open-ended and slightly harder. Looking at the three statements above shows that the number of white beans in the can is always reduced by two. So if \(N_w\) is the number of white beans in the can to begin with and \(B\) is the last remaining bean in the can then:
odd(\(N_w\)) \(\Rightarrow\)
    color(\(B\)) \(=\) WHITE

What about the reverse? Does:
even(\(N_w\)) \(\Rightarrow\)
    color(\(B\)) \(=\) BLACK

Since the number of beans is always reduced by one at each step and since the number of white beans is always reduced by two in step 2 above, then an even number of white beans to begin with will eventually result in a can filled with black beans and therefore step 3 of the algorithm will never be performed after that point. The algorithm will terminate with one black bean.
The statements can then be made:
odd(\(N_w\)) \(\Leftrightarrow\)
    color(\(B\)) \(=\) WHITE

even(\(N_w\)) \(\Leftrightarrow\)
    color(\(B\)) \(=\) BLACK