Professor Erasmus told me that today he has proved another fascinating theorem about strings made of 0s and 1s. He takes an arbitrary such string and repeats the following step on it:
- if the leftmost symbol is 1, Erasmus removes the three leftmost symbols and attaches 11 at the right end
- if the leftmost symbol is 0, Erasmus removes the three leftmost symbols and attaches 0010 at the right end
If the procedure ever reaches a string of length at most 2, it halts.
Example 1: Starting from 1001, this procedure yields 111, then 11, and halts.
Example 2: Starting from 01010, this procedure yields 100010, then 01011, then 110010, then again 01011, then again 110010; etc. There is a loop of length two.
Professor Erasmus has proved that independently of the starting string, the procedure will eventually halt or enter a loop of length at most 25.
Has the professor once again made one of his well-known mathematical blunders, or does his claimed theorem indeed hold true?