From 60e11de044fc3fa913e9ce040ee036354eb15659 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 5 Mar 2019 11:10:15 +0100
Subject: forward_simu_alt proof Asmblockdeps

---
 mppa_k1c/Asmblockdeps.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 273ccb68..4912a96f 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1300,11 +1300,16 @@ Proof.
   - congruence.
 Qed.
 
-Axiom forward_simu_alt:
+Theorem forward_simu_alt:
   forall rs1 m1 s1' b ge fn,
     Ge = Genv ge fn ->
     match_states (State rs1 m1) s1' -> 
     match_outcome (exec_bblock ge fn b rs1 m1) (exec Ge (trans_block b) s1').
+Proof.
+  intros until fn. intros GENV MS. destruct (exec_bblock _ _ _ _ _) eqn:EXEB.
+  - eapply forward_simu; eauto.
+  - eapply forward_simu_stuck; eauto.
+Qed.
 
 Local Hint Resolve trans_state_match.
 
-- 
cgit