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

Update

This commit is contained in:
Thomas Baruchel 2023-01-22 22:36:48 +01:00
parent 358404d2be
commit 0fe7e6dd25
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/thue_morse3.v
View File

@ -582,6 +582,8 @@ Proof.
apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_succ. reflexivity. easy. easy.
assert (H' := H).
(* SECOND PART PF THE PROOF: case b0 <> b1 *)
(* sinon, sur la base de T F T F || F T F T
quatre cas :
@ -956,6 +958,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite <- Nat.add_assoc. replace (2+8) with 10.
replace (8) with (2^3) at 1. rewrite <- Nat.pow_add_r.
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
rewrite <- tm_size_power2. rewrite H'. unfold lh.
rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
rewrite <- Nat.add_lt_mono_l. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ. apply Nat.le_refl.
apply Nat.lt_le_incl. assumption. reflexivity. reflexivity.
assumption. apply Nat.lt_0_succ.