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

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

diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 745b972..9e0c467 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1553,6 +1553,9 @@ Lemma tm_step_palindromic_even_morphism2 :
   -> (length a) mod 4 = 0
   -> 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))))))
      /\ 11 = 42.
 Proof.
   intros n hd a tl. intros H W J0.
@@ -1685,13 +1688,12 @@ Proof.
   assert (K': even (length (map negb (rev a'))) = true).
   rewrite map_length. rewrite rev_length. assumption.
 
-
-
-
   assert (Q: length hd' <= length (tm_step n)).
   rewrite H. rewrite app_length. apply Nat.le_add_r.
 
-
+  assert (Q': length hd' + length a' <= length (tm_step n)).
+  rewrite H. rewrite app_assoc. rewrite app_length.
+  rewrite <- app_length. apply Nat.le_add_r.
 
 
 
@@ -1788,29 +1790,31 @@ Proof.
 
 
   split.
-
   rewrite <- pred_Sn. rewrite <- pred_Sn.
   rewrite H4 at 1. fold hd'. rewrite H4'. unfold hd'.
   rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
   rewrite Nat.div_div. reflexivity. easy. easy.
   rewrite <- H6. assumption.
 
+  split.
+  rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H5 at 1. fold a'.
+  rewrite H5'. unfold a'.
+  rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
+  rewrite Nat.div_div.
+  replace (length hd / 4) with (Nat.div2 (length hd')). reflexivity.
+  replace 4 with (2*2). rewrite <- Nat.div_div.
+  rewrite <- Nat.div2_div. rewrite <- Nat.div2_div. rewrite <- H6. reflexivity.
+  easy. easy. reflexivity. easy. easy.
+  rewrite skipn_length.
+  apply Nat.le_add_le_sub_l.
+  rewrite <- H6. rewrite <- H7. assumption.
 
 
 
+Nat.div2 (length hd) + Nat.div2 (length a) <= length (tm_step (S n))
 
 
 
-
-
-  assert (hd = hd). reflexivity. rewrite H4 in H12 at 2. fold hd' in H12.
-  rewrite H4' in H12. unfold hd' in H12.
-  rewrite firstn_length_le in H12.
-  rewrite Nat.div2_div in H12.
-  rewrite Nat.div2_div in H12. rewrite Nat.div_div in H12.
-  replace (2*2) with 4 in H12.
-
-
 Admitted.