Update
This commit is contained in:
parent
458f9aa148
commit
a304f0a9a8
@ -908,7 +908,30 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||||||
rewrite H9.
|
rewrite H9.
|
||||||
apply eq_S in H9. rewrite <- Nat.add_1_r in 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 <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
|
||||||
rewrite H9. unfold lh.
|
rewrite H9. unfold lh. unfold hd'.
|
||||||
|
|
||||||
|
rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''.
|
||||||
|
rewrite app_length.
|
||||||
|
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
|
||||||
|
rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
|
||||||
|
rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
|
||||||
|
rewrite <- Nat.add_succ_r. rewrite Nat.add_sub.
|
||||||
|
rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. reflexivity.
|
||||||
|
apply Nat.le_refl. unfold lh in T.
|
||||||
|
rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm.
|
||||||
|
rewrite <- Nat.add_succ_comm. rewrite app_length in T.
|
||||||
|
assumption. reflexivity. rewrite Y''.
|
||||||
|
rewrite app_length.
|
||||||
|
replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
|
||||||
|
rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
|
||||||
|
rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
|
||||||
|
rewrite <- Nat.add_succ_r. rewrite Nat.add_sub.
|
||||||
|
apply Nat.le_succ_diag_r. rewrite Nat.add_succ_r.
|
||||||
|
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
|
||||||
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
|
||||||
|
rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4).
|
||||||
|
rewrite <- Nat.add_le_mono_r.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)
|
(* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)
|
||||||
|
Loading…
Reference in New Issue
Block a user