From c81fec4ebdff009537ac6c18b4f309f46545267b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 26 Nov 2022 06:01:17 +0100 Subject: [PATCH] Update --- thue-morse.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/thue-morse.v b/thue-morse.v index e42a995..a0e1d31 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1069,6 +1069,24 @@ Proof. apply H0. Qed. +Lemma tm_step_split_index : + forall (k b n m : nat), + S k < 2^m -> k = 2^n - 1 + 2^S n * b + -> nth_error (tm_step m) k = nth_error (tm_step m) (S k) + <-> odd n = true. +Proof. + intros k a b n m. intros H I J. + assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I. + apply tm_step_repunit. +ERREUR DANS l'énoncé : ce n'est pas Some odd mais lié à la parité du poids +de Hamming de b !!! + odd n XOR odd Hamming(b) + (chaque bit à 1 de b modifie) + o + +test = lambda b, n: t[ 2**n-1 + 2**(n+1) * b ] == t[ 2**n-1 + 2**(n+1) * b + 1] + +