From c10a003026e9d5422a3ad8c2f8e3ba69e5f16837 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sun, 22 Jan 2023 14:17:44 +0100
Subject: [PATCH] Update

---
 src/thue_morse3.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 8aaab1b..d0fc9ba 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -698,6 +698,17 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
 
   (* on étend hd *)
   destruct hd. inversion Q.
+  (* TODO : sortir les trucs de removelast *)
+  rewrite app_removelast_last
+      with (l := removelast (b3::b5::hd)) (d := false) in H.
+  assert ({last (removelast (b3 :: b5 :: hd)) false = b1}
+            + {~ last (removelast (b3 :: b5 :: hd)) false = b1}).
+  apply bool_dec. destruct H5. rewrite e0 in H.
+  rewrite <- app_assoc in H.
+  replace (b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl)
+    with ([b1] ++ b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1. reflexivity.
 
   (* on étend tl*)
   destruct tl.
@@ -718,12 +729,47 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
   apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
   apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
+  assert ({b6=b1} + {~ b6=b1}). apply bool_dec. destruct H5. rewrite e0 in H.
+  replace (
+    (removelast (removelast (b3 :: b5 :: hd)) ++
+     [last (removelast (b3 :: b5 :: hd)) false]) ++
+    [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b1 :: tl)
+    with (
+    (removelast (removelast (b3 :: b5 :: hd)) ++
+     [last (removelast (b3 :: b5 :: hd)) false] ++
+    [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: nil)
+      ++ [b1] ++ [b1] ++ [b1] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1.
+  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
+  rewrite <- app_assoc. reflexivity.
 
+  assert (b6 = b0). destruct b6; destruct b1; destruct b0.
+  reflexivity. contradiction n5. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n5. reflexivity. reflexivity.
+  rewrite H5 in H.
+  assert (last (removelast (b3 :: b5 :: hd)) false = b0).
+  destruct (last (removelast (b3 :: b5 :: hd)) false);
+  destruct b1; destruct b0.
+  reflexivity. contradiction n4. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n4. reflexivity. reflexivity.
+  rewrite H6 in H.
+
+  (* TODO : étendre encolre hd ??? *)
+  
 
 
 Admitted.
 
 
+                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
+                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
+                  FTTFTFFT FTTFTF  (pb avec le repeating_pattern de 8 ???)
+                     TFT TFT FF TFT TFT (si on part sur 2 mod 8)
+                                        (idem en partant de la droite pour 6 mod 8)
+Le lemme repeating_patterns se base sur les huit premiers termes de TM :