proposition: Lemma semax_ramification_P: forall Delta c (G L L' G': environ -> mpred), G |-- L * ModBox c (L' -* G') -> semax Delta L c (normal_ret_assert L') -> semax Delta G c (normal_ret_assert G').
proof: Proof. intros. apply semax_pre_post with (P' := L * ModBox c (L' -* G')) (R' := normal_ret_assert (L' * ModBox c (L' -* G'))). + intros. apply andp_left2. auto. + intros. apply andp_left2. apply normal_ret_assert_derives'. rewrite sepcon_comm, wand_sepcon_adjoint; auto. apply EnvironBox_T. apply vars_relation_Equivalence. + apply semax_frame with (F := ModBox c (L' -* G')) in H0. - rewrite frame_normal in H0. auto. - apply EnvironStable_var_relation_closed. apply EnvironBox_EnvironStable. apply vars_relation_Equivalence. Qed.
imports: CertiGraph.lib.Equivalence_ext CertiGraph.veric_ext.SeparationLogic VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.closed_lemmas VST.floyd.forward_lemmas