Update

thue-morse.v

@@ -1160,6 +1160,53 @@ Proof.
 Qed.
 
 
+Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool),
+  tm_step n = hd ++ a ++ a ++ a ++ tl
+  -> 0 < length a
+  -> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
+                         /\ length a = length b
+                         /\ even (length hd2) = true.
+Proof.
+  intros n a hd tl. intros H I.
+  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
+  apply Nat.Even_or_Odd.
+  destruct J.
+  - exists hd. exists a. exists tl.
+    split. assumption. split. reflexivity.
+    apply Nat.Even_EvenT in H0.
+    apply Nat.EvenT_even in H0. assumption.
+  - apply Nat.Odd_OddT in H0.
+    apply Nat.OddT_odd in H0.
+    rewrite <- Nat.negb_even in H0. rewrite negb_true_iff in H0.
+    destruct a.
+    + simpl in I. apply Nat.lt_irrefl in I. contradiction I.
+    + assert (Nat.even (length hd) = Nat.even (length tl)).
+      generalize I. generalize H. apply tm_step_cube2.
+      rewrite H0 in H1.
+      destruct tl.
+      * simpl in H1. inversion H1.
+      * assert (hd_error (b::a) = hd_error (b0::tl)).
+        generalize I. generalize H0. generalize H. apply tm_step_cube3.
+        simpl in H2. inversion H2. rewrite <- H4 in H.
+        exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl.
+        split. rewrite H.
+        rewrite app_assoc_reverse. apply app_inv_head_iff.
+        replace (b::a) with ([b] ++ a).
+        rewrite app_assoc_reverse. apply app_inv_head_iff.
+        rewrite app_assoc_reverse. rewrite app_assoc_reverse.
+        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
+        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
+        rewrite app_assoc_reverse. reflexivity.
+        reflexivity.
+        split. rewrite last_length. reflexivity.
+        rewrite last_length.
+        rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite H0.
+        reflexivity.
+Qed.
+
+
+
+