If you're given a binary string of the form $a_1a_2\ldots a_n \overline {a_1a_2\ldots a_n}$, will the following rule applied a finite number eventually lead to the string $0^n1^n$ where exponentiation means concatenation $n$ times. Rule:
1) Swap the bits in positions $a_n$ and $\overline{a_n}$ (the indices remain constant, i.e. the $n^{th}$ bit and the $2n^{th}$ bit)
2) Rotate the longest suffix of zeros to the beginning of the string.
Example on the string $000110111001$, applying first step we get $000111111000$ and then applying the second step we rotate the last 3 zeros and get $000000111111$.
I know that it makes intuitive sense that eventually you get to the $0^n1^n$, because you're kind of ironing out the zeros that are stuck between ones. But how would you formally prove that this always happens? Would it be some kind of inductive proof or a proof by contradiction?
We know that after the second step, the amount of $0$'s that our string is starting with has increased by at least $1$. Thus, we're done after at least $n$ steps, since then our string starts with at least $n$ zeroes. And since we have exactly $n$ zeroes, we have the string $0^n1^n$.