Intertwining of Complementary Thue-Morse Factors

Abstract

We consider the positions of occurrences of a factor $x$ and its binary complement $\overline{x}$ in the Thue-Morse word $\mathbf{t}=01101001\cdots$, and show that these occurrences are "intertwined" in essentially two different ways. Our proof method consists of stating the needed properties as a first-order logic formula $\phi$, and then using a theorem-prover to prove $\phi$.