From 7d3ac44ff5b909a6d00a94e6d30748e15054daf5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:54:40 +0100
Subject: FINISHED the forward-moves pass

---
 backend/ForwardMovesproof.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'backend/ForwardMovesproof.v')

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:
-- 
cgit