Update
This commit is contained in:
parent
c10a003026
commit
4e36a9abed
|
@ -744,6 +744,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
||||||
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
||||||
rewrite <- app_assoc. reflexivity.
|
rewrite <- app_assoc. reflexivity.
|
||||||
|
|
||||||
|
(* on assigne les valeurs correctes aux deux extrémités *)
|
||||||
assert (b6 = b0). destruct b6; destruct b1; destruct b0.
|
assert (b6 = b0). destruct b6; destruct b1; destruct b0.
|
||||||
reflexivity. contradiction n5. reflexivity. reflexivity.
|
reflexivity. contradiction n5. reflexivity. reflexivity.
|
||||||
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
||||||
|
@ -757,10 +758,15 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
||||||
reflexivity. contradiction n4. reflexivity. reflexivity.
|
reflexivity. contradiction n4. reflexivity. reflexivity.
|
||||||
rewrite H6 in H.
|
rewrite H6 in H.
|
||||||
|
|
||||||
(* TODO : étendre encolre hd ??? *)
|
(* on étend hd *)
|
||||||
|
destruct hd. simpl in H. assert (odd 3 = true). reflexivity.
|
||||||
|
rewrite <- tm_step_pred with (n := n) (k := 0) in H7.
|
||||||
|
rewrite H in H7. simpl in H7. inversion H7. rewrite H9 in n1.
|
||||||
|
contradiction n1. reflexivity. simpl.
|
||||||
|
|
||||||
|
|
||||||
|
False, True, True, False, True, False, False, True, True, False, False
|
||||||
|
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user