Update

thue-morse.v

@@ -1069,6 +1069,27 @@ Proof.
       apply H0.
 Qed.
 
+Lemma tm_step_split_index :
+  forall (k b n m : nat),
+  S k < 2^m -> k = 2^n - 1 + 2^S n * b
+    -> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
+      <-> odd n = true.
+Proof.
+  intros k a b n m. intros H I J.
+  assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
+  apply tm_step_repunit.
+
+
+
+
+
+
+
+
+
+
+
+