Update

src/thue_morse2.v

@@ -79,17 +79,6 @@ Proof.
 Qed.
 
 
-
-
-
-
-  
-
-Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
-  tm_step n = hd ++ tl -> even (length hd) = true
-  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
-
-
 Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl -> length a = 3
   -> a = true::false::true::nil \/ a = false::true::false::nil.
@@ -116,10 +105,72 @@ Proof.
         apply Nat.succ_inj in I. apply Nat.succ_inj in I.
         rewrite length_zero_iff_nil in I. rewrite I. reflexivity.
 
+        replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl)
+          with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H.
+        apply tm_step_consecutive_identical in H.
+        rewrite J in H. simpl in H. inversion H.
 
-
-        rewrite app_assoc_reverse.
+        apply app_inv_head_iff. rewrite <- app_assoc_reverse.
+        apply app_inv_head_iff. reflexivity.
+      * destruct a. inversion I. simpl in I.
+        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+        apply Nat.succ_inj in I. apply length_zero_iff_nil in I.
+        destruct b. rewrite I. reflexivity.
+        rewrite I in H.
+        replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl)
+          with ((hd ++ [true]) ++ [false;false] ++ [true] ++ [false;false] ++ tl) in H.
+        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
+        rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity.
+    + right. destruct a. inversion I. destruct b.
+      * destruct a. inversion I. simpl in I.
+        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+        apply Nat.succ_inj in I. apply length_zero_iff_nil in I.
+        destruct b. rewrite I in H.
+        replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl)
+          with ((hd ++ [false]) ++ [true;true] ++ [false] ++ [true;true] ++ tl) in H.
+        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
+        rewrite app_assoc_reverse. apply app_inv_head_iff. reflexivity.
+        rewrite I. reflexivity.
+      * replace (hd ++ (false::false::a) ++ (false::false::a) ++ tl)
+          with (hd ++ (false::false::nil) ++ a ++ (false::false::nil) ++ (a ++ tl)) in H.
+        apply tm_step_consecutive_identical in H. simpl in H. inversion H.
+        simpl in I. apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+        rewrite I in H. inversion H.
         apply app_inv_head_iff.
+        rewrite <- app_assoc_reverse.
+        apply app_inv_head_iff. reflexivity.
+Qed.
+
+
+
+
+
+
+
+        destruct a. inversion I.
+        destruct b.
+        assert (K: tm_step n = hd ++ [false] ++ [true] ++ [true]
+                               ++ a ++ [true] ++ [true] ++ [true] ++ a ++ tl).
+        rewrite H. apply app_inv_head_iff.
+        replace (true::true::true::a) with ([true] ++ [true] ++ [true] ++ a).
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. apply app_inv_head_iff.
+        rewrite <- app_assoc. reflexivity. reflexivity.
+        apply tm_step_cubefree in K. contradiction K. reflexivity.
+        simpl. apply Nat.lt_0_1. simpl in I. apply Nat.succ_inj in I.
+        apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+        rewrite length_zero_iff_nil in I. rewrite I. reflexivity.
+
+        replace (hd ++ (true::true::a) ++ (true::true::a) ++ tl)
+          with (hd ++ (true::true::nil) ++ (a ++ (true::true::a) ++ tl)) in H.
+        apply tm_step_consecutive_identical in H.
+        rewrite J in H. simpl in H. inversion H.
+
+        apply app_inv_head_iff. rewrite <- app_assoc_reverse.
+        apply app_inv_head_iff. reflexivity.