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 21:03:18 +01:00
parent 2f6a74098a
commit 458f9aa148
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/thue_morse3.v
View File

@ -902,9 +902,16 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
assert (nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 3)
= nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 4)).
rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
rewrite H.
rewrite H. rewrite Nat.mul_comm.
apply eq_S in H9. symmetry in H9. rewrite <- Nat.add_1_r in H9.
rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
rewrite H9.
apply eq_S in H9. rewrite <- Nat.add_1_r in H9.
rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
rewrite H9. unfold lh.
(* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)
Lemma tm_step_repeating_patterns :