Update

src/thue_morse.v

@@ -340,6 +340,16 @@ Proof.
     simpl. rewrite negb_involutive. reflexivity.
 Qed.
 
+Lemma tm_morphism_twice_rev : forall (l : list bool),
+  rev (tm_morphism (tm_morphism l)) = tm_morphism (tm_morphism (rev l)).
+Proof.
+  intro l. induction l.
+  - reflexivity.
+  - simpl. rewrite tm_morphism_app. rewrite tm_morphism_app.
+    rewrite <- IHl. rewrite <- app_assoc. rewrite <- app_assoc.
+    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

@@ -211,7 +211,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma tm_step_palindromic_even_center :
+Theorem tm_step_palindromic_even_center :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
   -> 0 < length a
@@ -1852,9 +1852,58 @@ Qed.
 
 
 
+Lemma xxx :
+  forall (m n k : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> 6 < length a
+    -> length a = 2^(Nat.double m)
+    -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0.
+Proof.
+  intros m n k hd a tl. intros H I J.
+
+  destruct m. rewrite J in I. inversion I. inversion H1.
+  destruct m. rewrite J in I. inversion I. inversion H1.
+  inversion H3. inversion H5. inversion H7.
+
+  assert (W: (length a) mod 4 = 0).
+  rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
+  rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
+  rewrite Nat.mul_assoc in J.
+  replace (2*2) with 4 in J. rewrite J.
+  rewrite <- Nat.mul_mod_idemp_l. reflexivity.
+  easy. reflexivity. apply le_0_n. apply le_0_n.
+
+  assert (
+     hd = tm_morphism (tm_morphism (firstn (length hd / 4)
+           (tm_step (pred (pred n)))))
+     /\ a = tm_morphism (tm_morphism
+           (firstn (length a / 4) (skipn (length hd / 4)
+           (tm_step (pred (pred n))))))
+     /\ tl = tm_morphism (tm_morphism
+           (skipn (length hd / 4 + Nat.div2 (length a))
+             (tm_step (pred (pred n)))))).
+  generalize W. generalize I. generalize H.
+  apply tm_step_palindromic_even_morphism2.
+  destruct H0 as [K H0]. destruct H0 as [L M].
+
+  assert (V: 3 < n). generalize I. generalize H.
+  apply tm_step_palindromic_length_12_n.
+
+  induction m.
+  - rewrite K in H. rewrite L in H. rewrite M in H.
+    rewrite tm_morphism_twice_rev in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
 
 
 
+Theorem tm_step_palindromic_even_center :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> 0 < length a
+  -> even (length (hd ++ a)) = true.
+
 
 
 
@@ -1891,6 +1940,7 @@ Proof.
              (tm_step (pred (pred n)))))).
   generalize W. generalize I. generalize H.
   apply tm_step_palindromic_even_morphism2.
+  destruct H0 as [K H0]. destruct H0 as [L M].