Update

thue-morse.v

@@ -1064,8 +1064,74 @@ Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
 Proof.
   intros n m k. intros H.
   assert (I := H). apply Nat.lt_succ_l in I.
+  assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
+  rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
+  assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
+
+  (*
+Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
+  S k < 2^n ->
+    nth_error (tm_step n) k = nth_error (tm_step n) (S k)
+    <->
+    nth_error (tm_step (S n)) (k + 2^n)
+      = nth_error (tm_step (S n)) (S k + 2^n).
+   *)
 
   split.
+  - induction m.
+    + intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
+    apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+    apply K.
+    rewrite <- tm_step_next_range2_neighbor'.
+    apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+    apply K.
+    rewrite <- tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+    rewrite <- tm_step_next_range2_neighbor'. apply L.
+    apply H. rewrite <- Nat.add_succ_l. apply K.
+    rewrite <- Nat.add_succ_l. apply K.
+    + intros L.
+
+      rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
+
+      assert (S k < 2^(S n + m)).
+      assert (2^n < 2^(S n + m)).
+      assert (n < S n + m). assert (n < S n). apply Nat.lt_succ_diag_r.
+      generalize H0. apply Nat.lt_lt_add_r.
+      generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+      generalize H0. generalize H. apply Nat.lt_trans.
+      assert (H1 := H0). apply Nat.lt_succ_l in H1.
+
+      rewrite <- tm_step_next_range2_neighbor'.
+
+      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
+      generalize H1. generalize I. apply tm_step_stable.
+      assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
+      generalize H0. generalize H. apply tm_step_stable.
+      rewrite <- H2. rewrite <- H3. apply L.
+
+      apply H0.
+  -
+
+
+
+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.
+
+
+
+
+
+      rewrite <- Nat.add_succ_l.
+      replace (2^(n + S m)) with (2^(n+m) + 2^(n+m)).
+      rewrite Nat.add_assoc.
+      rewrite Nat.add_assoc.
+      (* rewrite Nat.add_succ_r. *)
+      generalize L.
+    apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+
+
+
+
   - assert (k < length (tm_step n)). rewrite tm_size_power2. apply I.
     apply nth_error_nth' with (d :=false) in H0.
     assert (S k < length (tm_step n)). rewrite tm_size_power2. apply H.