From 6ccbfa81a46644acd68179e676c43f138a05b289 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 23 Jan 2023 22:22:56 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 75a0b03..37726c6 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1176,7 +1176,36 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H. + pose (h0 := firstn (Nat.div2 (length hd'')) (tm_step n)). + pose (s0 := firstn (Nat.div2 (length s)) + (skipn (Nat.div2 (length hd'')) (tm_step n))). + pose (t0 := skipn (Nat.div2 (length s)) + (skipn (Nat.div2 (length hd'')) (tm_step n))). + fold h0 in H. fold s0 in H. fold t0 in H. + (* fin de la preuve pour cette partie : morphisme impossible *) + assert (s0 = [b0;b0;b1;b1;b0;b0;b1;b1]). fold s0 in H15. + unfold s in H15. destruct s0. inversion H15. + destruct s0. inversion H15. destruct s0. inversion H15. + destruct s0. inversion H15. destruct s0; inversion H15. + destruct s0. inversion H15. destruct s0. inversion H15. + destruct s0. inversion H15. destruct s0; inversion H15. + inversion H15. reflexivity. +(* + assert (b13 = b0). destruct b13; destruct b1; destruct b0. + reflexivity. inversion H46. reflexivity. inversion H45. + inversion H45. reflexivity. inversion H45. reflexivity. + rewrite H17 in H15. rewrite H17 in H47. rewrite <- H47 in H15. + rewrite <- H47 in H33. rewrite <- H33 in H15. + rewrite <- H47 in H24. rewrite <- H24 in H15. + rewrite <- H47 in H26. rewrite <- H26 in H15. + rewrite <- H47 in H39. rewrite <- H39 in H15. + rewrite <- H47 in H41. rewrite <- H41 in H15. + rewrite <- H47 in H43. rewrite <- H43 in H15. + rewrite negb_involutive in H15. rewrite negb_involutive in H15. + fold s in H15. + *) + rewrite H17 in H. Lemma tm_morphism_app : forall (l1 l2 : list bool),