From c78393a5d4d13d0f2cd7f0a73756d6bb598b5ae4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 9 May 2021 22:41:40 +0200 Subject: mib_exit draft --- scheduling/RTLtoBTLproof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') 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 *) -- cgit