diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 023837f9..1db088d2 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -264,12 +264,13 @@ Proof. - (* mib_BF *) admit. - (* mib_exit *) - (* destruct t. - 2: { + (* + simpl in *. + eapply iblock_istep_run_equiv in BTL_RUN. + inv BTL_RUN. eexists; left. eexists; split. + eapply exec_iblock; eauto. econstructor; repeat eexists. - eapply iblock_istep_run_equiv; eauto. inv STEP. eapply exec_Bgoto.*) admit. - (* mib_seq *) |