Update

thue-morse.v

@@ -982,7 +982,6 @@ Proof.
     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)
@@ -1028,42 +1027,6 @@ Qed.
 
 
 
-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. 
-    assert (I : 
-      eqb (nth (k + 2 ^ n) (tm_step (S n + m)) false)
-        (nth (S k + 2 ^ n) (tm_step (S n + m)) false)
-        =
-eqb (nth (k + 2 ^ n) (tm_step (S (S n + m))) false)
-  (nth (S k + 2 ^ n) (tm_step (S (S n + m))) false)
-  ).
-  assert (S k < 2^(S n + m)).
-  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.
-  + 
-
-    generalize H0.
-apply tm_step_next_range2_neighbor.
-
-
-
 
 Lemma tm_step_consecutive_power2 :
   forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),