Update

thue-morse.v

@@ -974,9 +974,59 @@ Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
   S k < 2^n ->
     eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
     = eqb
-    (nth (k + 2^n) (tm_step (S n+m)) false) (nth (S k + 2^n) (tm_step (S n+m)) false).
+    (nth (k + 2^(n+m)) (tm_step (S n+m)) false) (nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
 Proof.
-  intros n m k. intros H.
+  intros n m k. intros H. induction m.
+  - rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply tm_step_next_range2_neighbor.
+    apply H.
+  - rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
+    assert (I : eqb (nth k (tm_step (S n + m)) false)
+                    (nth (S k) (tm_step (S n + m)) false)
+              = eqb (nth (k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)
+                    (nth (S k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)).
+    apply tm_step_next_range2_neighbor. induction m.
+    + rewrite Nat.add_0_r. simpl. generalize H.
+      apply Nat.lt_lt_add_r.
+    + assert (2^n < 2^(S n + S m)).
+      assert (n < S n + S m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
+      apply Nat.pow_lt_mono_r. generalize H0. generalize H.
+      apply Nat.lt_trans.
+    + rewrite <- I. rewrite <- IHm.
+      assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
+      assert (K: k < 2^(S n+m)).
+      assert (L: 2^n < 2^(S n + m)).
+      assert (M: n < S n + m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
+      generalize L. generalize J. apply Nat.lt_trans.
+
+
+
+
+      generalize K. generalize J.
+      apply tm_step_stable.
+
+
+Theorem tm_step_stable : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
+
+
+
+
+
+
+
+Lemma tm_step_next_range2_neighbor : forall (n k : nat),
+  S k < 2^n ->
+    eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
+    = eqb
+    (nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
+
+
+
+
   induction m.
   - rewrite Nat.add_0_r. generalize H. apply tm_step_next_range2_neighbor.
   - rewrite Nat.add_succ_r. 
@@ -999,6 +1049,9 @@ eqb (nth (k + 2 ^ n) (tm_step (S (S n + m))) false)
     apply Nat.lt_trans.
   + 
 
+    generalize H0.
+apply tm_step_next_range2_neighbor.
+