Update

thue-morse.v

@@ -980,6 +980,30 @@ Proof.
   - 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: S k < 2^(S n + m)).
+
+      assert (2^n < 2^(S n + m)).
+      assert (n < S n + 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 I.
+
+    apply tm_step_next_range2_neighbor. induction m.
+
+  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).
+
+
+
+     *)
+
+
     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)
@@ -1002,18 +1026,56 @@ Proof.
       apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
       generalize L. generalize J. apply Nat.lt_trans.
 
+      assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
+      generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
+      assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)).
+      generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
+
+      (*  assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false).  *)
+      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
+      generalize K. generalize J. apply tm_step_stable.
+
+      rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
+      replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)) in H4.
+      rewrite H4.
+
+      assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
+      generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
+      assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
 
 
+      assert (2^n < 2^(S n + m)).
+      assert (n < S n + m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      generalize H5.
+      apply Nat.pow_lt_mono_r.
+      apply Nat.lt_1_2.
+      assert (S k < 2^(S n + m)). generalize H5. generalize H.
+      apply Nat.lt_trans.
 
-      generalize K. generalize J.
+      generalize H6. rewrite <- tm_size_power2. apply nth_error_nth'.
-      apply tm_step_stable.
 
       
-Theorem tm_step_stable : forall (n m k : nat),
+      assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
-  k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
+      assert (2^n < 2^(S n + m)).
+      assert (n < S n + m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      generalize H6.
+      apply Nat.pow_lt_mono_r.
+      apply Nat.lt_1_2.
+      assert (S k < 2^(S n + m)). generalize H6. generalize H.
+      apply Nat.lt_trans.
 
+      generalize H7. generalize H. apply tm_step_stable.
+      rewrite H3 in H6. rewrite H5 in H6.
+      inversion H6. rewrite H8.
 
+      replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)).
+      reflexivity.
 
+      reflexivity.
+      reflexivity.
+Qed.