Update

src/thue_morse.v

@@ -172,7 +172,6 @@ Proof.
     rewrite negb_involutive. reflexivity.
 Qed.
 
-
 Lemma tm_build_negb : forall (l : list bool),
   tm_morphism (map negb l) = map negb (tm_morphism l).
 Proof.
@@ -331,6 +330,16 @@ Proof.
   rewrite app_inv_head_iff in L. assumption.
 Qed.
 
+Lemma tm_morphism_rev2 : forall (l : list bool),
+  map negb (rev (tm_morphism l)) = tm_morphism (rev l).
+Proof.
+  intro l. induction l.
+  - reflexivity.
+  - simpl. rewrite tm_morphism_app. rewrite <- IHl.
+    rewrite map_app. rewrite map_app. rewrite <- app_assoc.
+    simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
 
 (**
    Lemmas and theorems below are related to the second function defined initially.

src/thue_morse3.v

@@ -1613,6 +1613,67 @@ Proof.
   assert (K': even (length (map negb (rev a'))) = true).
   rewrite map_length. rewrite rev_length. assumption.
 
+  assert (H0': even (length (hd' ++ a')) = true).
+  rewrite app_length. rewrite Nat.even_add.
+  rewrite I'. rewrite J'. reflexivity.
+
+
+
+
+
+
+  destruct n. inversion V. inversion H10.
+  rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
+
+  assert (H1': hd' ++ a' = tm_morphism (firstn (Nat.div2 (length (hd' ++ a')))
+                                  (tm_step n))).
+  generalize H0'. generalize H. apply tm_morphism_app2.
+
+  rewrite <- app_assoc in H. symmetry in H1'.
+  assert (H2': even (length (hd' ++ a' ++ (map negb (rev a')))) = true).
+  rewrite app_length. rewrite Nat.even_add. rewrite I'.
+  rewrite app_length. rewrite Nat.even_add. rewrite J'. rewrite K'.
+  reflexivity.
+
+  assert (H3': tl' = tm_morphism (skipn
+       (Nat.div2 (length (hd' ++ a' ++ (map negb (rev a')))))
+                         (tm_step n))).
+  replace (hd' ++ a' ++ (map negb (rev a')) ++ tl')
+      with ((hd' ++ a' ++ (map negb (rev a'))) ++ tl') in H.
+  generalize H2'. generalize H. apply tm_morphism_app3.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+
+  assert (H4': hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))).
+  generalize I'. generalize H. apply tm_morphism_app2.
+
+  assert (H5': a' = tm_morphism (skipn (Nat.div2 (length hd'))
+           (firstn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))).
+  generalize I'. generalize H1'. apply tm_morphism_app3.
+
+  rewrite skipn_firstn_comm in H5'. rewrite app_length in H5'.
+
+  replace (Nat.div2 (length hd' + length a'))
+    with ((length hd') / 2 + Nat.div2 (length a')) in H5'.
+  rewrite <- Nat.div2_div in H5'. rewrite Nat.add_sub_swap in H5'.
+  rewrite Nat.sub_diag in H5'. rewrite Nat.add_0_l in H5'.
+
+  rewrite H4' in H. rewrite H5' in H. rewrite H3' in H.
+  rewrite tm_morphism_rev2 in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H.
+
+  rewrite app_length in H. rewrite app_length in H.
+  rewrite map_length in H. rewrite rev_length in H.
+  replace (length a' + length a') with ((length a')*2) in H.
+  replace (Nat.div2 (length hd' + length a' * 2))
+    with ((length hd' + length a' * 2) / 2) in H.
+  rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
+
+
+
+
+
+
 
 Admitted.