diff options
| -rw-r--r-- | backend/ForwardMovesproof.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 8c036851..826d4250 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -475,7 +475,11 @@ Proof. apply move_ok. assumption. } - admit. + rewrite KILL in GE. + apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). + assumption. + apply kill_ok. + assumption. (* load *) - econstructor; split. @@ -762,7 +766,7 @@ Proof. destruct (map # pc) as [mpc |] in *; try contradiction. destruct H8 as [rel' RGE]. eapply get_rb_killed; eauto. -Admitted. +Qed. Lemma transf_initial_states: |