baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-11-26 06:01:41 +01:00
parent c81fec4ebd
commit f314138731
1 changed files with 9 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
thue-morse.v
View File

@ -1078,13 +1078,16 @@ 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]