From c7bad77004271f3037305f483d5de2c1f8cc45d0 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Fri, 27 Jan 2023 10:11:47 +0100
Subject: [PATCH] Update

---
 src/thue_morse3.v | 39 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 34 insertions(+), 5 deletions(-)

diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 87c11d7..4f4d34e 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1617,11 +1617,6 @@ Proof.
   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.
 
@@ -1675,6 +1670,40 @@ Proof.
 
 
 
+
+  pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)).
+  pose (a'' := firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd'))
+            (tm_step n))).
+  pose (tl'' := skipn (Nat.div2 (length hd') + length a') (tm_step n)).
+  fold hd'' in H. fold a'' in H. fold tl'' in H.
+
+  assert (length hd'' = Nat.div2 (length hd')). unfold hd''. rewrite H4'.
+  rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
+  replace (min (Nat.div2 (length hd')) (length (tm_step n)))
+    with (min (length (tm_step n)) (Nat.div2 (length hd'))).
+  rewrite Nat.min_comm. rewrite Nat.min_assoc. rewrite Nat.min_id.
+  reflexivity. rewrite Nat.min_comm. reflexivity.
+
+  assert (length a'' = Nat.div2 (length a')). unfold a''. rewrite H5'.
+  rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
+  rewrite Nat.min_comm. rewrite <- H9.
+  replace
+    (min (Nat.div2 (length a')) (length (skipn (length hd'') (tm_step n))))
+    with 
+    (min (length (skipn (length hd'') (tm_step n))) (Nat.div2 (length a'))).
+  rewrite Nat.min_assoc. rewrite Nat.min_id. reflexivity.
+  rewrite Nat.min_comm. reflexivity.
+
+  assert (length tl'' = Nat.div2 (length tl')). unfold tl''. rewrite H3'.
+  rewrite tm_morphism_length_half. rewrite app_length.
+  symmetry. rewrite Nat.div2_div.
+  rewrite app_length. rewrite map_length. rewrite rev_length.
+  replace (length a' + length a') with (length a' * 2).
+  rewrite Nat.div_add. rewrite <- Nat.div2_div. reflexivity. easy.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+
+
+
 Admitted.