jff's conjecture

Joao F. Ferreira asks the question:

Given a finite binary string, repeatedly change a pattern 00 to 01 or 11 to 10.  Will you ever stop?

Theorem: yes, always.

Proof: By strong induction on the length of n: any series of valid substitutions on any string of length n eventually terminates.

Notice that both substitutions keep the first character fixed.  For example, if the string starts with 01, then no substitution
will ever make it start with anything but 01.  

Therefore, if the string starts with 01 or 10, we are done, by appealing to the IH on the remainder (= all but the first character). 

If the string starts with 00 or 11, then when one of these is substituted it becomes 01 or 10, and then we appeal to the IH
on the remainder.  To see that these must eventually be substituted, we again appeal to the IH on the remainder -- i.e.
eventually there will be no more substitutions in the remainder and we will be forced to do this one.