diff options
Diffstat (limited to 'mppa_k1c/abstractbb/DepTreeTheory.v')
| -rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index bfe79d42..bf45d11a 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -352,11 +352,11 @@ Proof. Qed. -Theorem bblock_deps_equiv p1 p2: +Theorem bblock_deps_simu p1 p2: (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x) - -> bblock_equiv ge p1 p2. + -> bblock_simu ge p1 p2. Proof. - intros H m2. + intros H m2 DONTFAIL. remember (run ge p1 m2) as om1. destruct om1; simpl. + apply bblock_deps_Some_correct2. |