From 354a87fddc668a0df695ed2e99310a4e8743dfc9 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 14 Dec 2022 20:29:05 +0100 Subject: [PATCH] Update --- thue-morse.v | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index e521677..473146c 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1152,14 +1152,11 @@ Proof. rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2. assert (forall a b, option_map negb a = option_map negb b <-> a = b). - intros a b. destruct a. destruct b. destruct b0. destruct b. - simpl. split. intro. reflexivity. intro. reflexivity. - simpl. split. intro. inversion H2. intro. inversion H2. - destruct b. simpl. split. intro. inversion H2. intro. inversion H2. - simpl. split. intro. reflexivity. intro. reflexivity. - split. intro. inversion H2. intro. inversion H2. - destruct b. split. intro. inversion H2. intro. inversion H2. - split. intro. reflexivity. intro. reflexivity. + intros a b. destruct a. destruct b. destruct b0. + destruct b; simpl. split; intro; reflexivity. split; intro; inversion H2. + destruct b; simpl. split; intro; inversion H2. split; intro; reflexivity. + split; intro; inversion H2. + destruct b. split; intro; inversion H2. split; intro; reflexivity. replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i). replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).