From a3e8c156277af593cb5b0c0093ee6f7b165d4fa6 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 2 Feb 2023 18:48:40 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index a71a420..d1ef1a1 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2209,6 +2209,20 @@ Proof. reflexivity. contradiction H6. reflexivity. reflexivity. rewrite H7 in H. + assert ({b=b6} + {~ b=b6}). apply bool_dec. destruct H8. rewrite e in H. + replace (hd ++ [b6; b6; b6; b5; b6; b5; b5; b6] + ++ [b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) + with (hd ++ [b6] ++ [b6] ++ [b6] + ++ [b5; b6;b5;b5;b6;b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) in H. + apply tm_step_cubefree in H. contradiction H. reflexivity. + apply Nat.lt_0_1. reflexivity. + + assert (b = b5). destruct b; destruct b5; destruct b6. + reflexivity. reflexivity. contradiction n1. reflexivity. + contradiction H1. reflexivity. contradiction H1. reflexivity. + contradiction n1. reflexivity. reflexivity. reflexivity. + rewrite H8 in H. + (* Lemma tm_step_proper_palindrome_center : forall (m n k : nat) (hd a tl : list bool),