Update

src/thue_morse3.v

@@ -307,8 +307,8 @@ Qed.
 *)
 
 
-(* palidrome 2*4 : soit centré en 4n+2 soit pas plus de 2*4 *)
-(* on prouve facilement que hd != nil *)
+(* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *)
+(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème *)
 Lemma tm_step_palindromic_length_8 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
@@ -673,20 +673,23 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
   contradiction n3. reflexivity. reflexivity. reflexivity.
   rewrite H3 in H. rewrite H2 in H.
 
+  assert (b2 = b0). destruct b2; destruct b1; destruct b0.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  rewrite H4 in H.
 
-
-Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
-    tm_step n' = w ++ z ++ y
-    -> length z = 4 -> length w mod 4 = 3
-    -> exists (x : bool), skipn 2 z = [x;x].
-
-
-  rewrite app_length in H1. rewrite app_length in H1.
-  rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
-  rewrite H2 in H1. inversion H1. easy. easy. easy.
-
-
-
+  (* dernier cas (difficile
+                (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
+                remarquer le schéma    a ++ (rev a) ++ a
+     apparaît jusqu'à six termes à gauche et à droite
+     empiriquement : n'apparaît jamais avec un 7ème palindromique ajouté
+                   remonter encore d'un cran et prouver la différence à ce stade,
+                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
+                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
+                     TFT TFT FF TFT TFT
+                     revoir l'énoncé en fonction
+  *)