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 2023-01-22 19:19:39 +01:00
parent 27b630570b
commit 52b462d85c
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/thue_morse3.v
View File

@ -860,7 +860,18 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite e0 in H7. inversion H7. assumption.
easy.
(* inutile
assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
*)
(* analyse finale *)
assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H.
(* premier sous-cas : b8 = b9, contradiction lié à repeating_patterns *)
assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H7. rewrite e1 in H.
(* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
(* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
False, True, True, False, True, False, False, True, True, False, False