From 98843bb92d75d6fe705c3c7220fe7c73cbbe741e Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Thu, 2 Feb 2023 10:22:38 +0100
Subject: [PATCH] Update

---
 src/thue_morse2.v |  2 ++
 src/thue_morse3.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)

diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index 90334ae..6f4c1b5 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -15,6 +15,8 @@
      parity than the length of the factor being squared)
    - tm_step_square_prefix_not_nil (no square at the beginning
      of the sequence)
+   - tm_step_square_tail_not_nil (no square at the end
+     of the partial sequence)
 *)  
 
 Require Import thue_morse.
diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index f8d82ca..c28ebe2 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -2096,6 +2096,52 @@ Proof.
 Qed.
 
 
+Lemma tm_step_non_proper_palindrome_16 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> length a = 8
+  -> skipn (length hd - 8) hd = rev (firstn 8 tl).
+Proof.
+  intros n hd a tl. intros H I.
+
+  assert (J: length a mod 4 = 0). rewrite I. reflexivity.
+  assert (K := J).
+  rewrite tm_step_palindromic_length_12_prefix
+    with (n := n) (hd := hd) (tl := tl) in K.
+
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+
+  destruct a.
+  replace (rev [b; b0; b1; b2; b3; b4; b5; b6])
+    with ([b6; b5; b4; b3; b2; b1; b0; b]) in H.
+
+  assert (b4 = b5).
+  replace (hd ++ [b; b0; b1; b2; b3; b4; b5; b6]
+      ++ [b6; b5; b4; b3; b2; b1; b0; b] ++ tl)
+    with ((hd ++ [b; b0; b1]) ++ [b2; b3; b4; b5]
+      ++ [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl) in H.
+  assert (length (hd ++ [b; b0; b1]) mod 4 = 3).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K.
+  reflexivity. easy.
+  assert (exists x, skipn 2 [b2; b3; b4; b5] = [x; x]).
+  generalize H0.
+  apply tm_step_factor4_3mod4 with (n' := n)
+    (y := [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption.
+  reflexivity. destruct H1. inversion H1. reflexivity.
+  rewrite <- app_assoc. reflexivity. rewrite H0 in H.
+
+  assert (b5 <> b3).
+  replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
+      ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
+    with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6])
+      ++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H.
+  apply tm_step_cubefree in H.
+
+
+
 
 (*
 Lemma tm_step_proper_palindrome_center :